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 (U21 1) 0.002/0.002 (U22 1) 0.002/0.002 (U31 1) 0.002/0.002 (U41 1) 0.002/0.002 (U42 1) 0.002/0.002 (U51 1) 0.002/0.002 (U52 1) 0.002/0.002 (U61 1) 0.002/0.002 (U71 1) 0.002/0.002 (U72 1) 0.002/0.002 (U81 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 (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) -> tt 0.002/0.002 U21(tt,V2:S) -> U22(isList(V2:S)) 0.002/0.002 U22(tt) -> tt 0.002/0.002 U31(tt) -> tt 0.002/0.002 U41(tt,V2:S) -> U42(isNeList(V2:S)) 0.002/0.002 U42(tt) -> tt 0.002/0.002 U51(tt,V2:S) -> U52(isList(V2:S)) 0.002/0.002 U52(tt) -> tt 0.002/0.002 U61(tt) -> tt 0.002/0.002 U71(tt,P:S) -> U72(isPal(P:S)) 0.002/0.002 U72(tt) -> tt 0.002/0.002 U81(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(isList(V1:S),V2:S) 0.002/0.002 isList(nil) -> tt 0.002/0.002 isList(V:S) -> U11(isNeList(V:S)) 0.002/0.002 isNeList(__(V1:S,V2:S)) -> U41(isList(V1:S),V2:S) 0.002/0.002 isNeList(__(V1:S,V2:S)) -> U51(isNeList(V1:S),V2:S) 0.002/0.002 isNeList(V:S) -> U31(isQid(V:S)) 0.002/0.002 isNePal(__(I:S,__(P:S,I:S))) -> U71(isQid(I:S),P:S) 0.002/0.002 isNePal(V:S) -> U61(isQid(V:S)) 0.002/0.002 isPal(nil) -> tt 0.002/0.002 isPal(V:S) -> U81(isNePal(V:S)) 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 (U21 1) 0.002/0.002 (U22 1) 0.002/0.002 (U31 1) 0.002/0.002 (U41 1) 0.002/0.002 (U42 1) 0.002/0.002 (U51 1) 0.002/0.002 (U52 1) 0.002/0.002 (U61 1) 0.002/0.002 (U71 1) 0.002/0.002 (U72 1) 0.002/0.002 (U81 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 (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) -> tt 0.002/0.002 U21(tt,V2:S) -> U22(isList(V2:S)) 0.002/0.002 U22(tt) -> tt 0.002/0.002 U31(tt) -> tt 0.002/0.002 U41(tt,V2:S) -> U42(isNeList(V2:S)) 0.002/0.002 U42(tt) -> tt 0.002/0.002 U51(tt,V2:S) -> U52(isList(V2:S)) 0.002/0.002 U52(tt) -> tt 0.002/0.002 U61(tt) -> tt 0.002/0.002 U71(tt,P:S) -> U72(isPal(P:S)) 0.002/0.002 U72(tt) -> tt 0.002/0.002 U81(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(isList(V1:S),V2:S) 0.002/0.002 isList(nil) -> tt 0.002/0.002 isList(V:S) -> U11(isNeList(V:S)) 0.002/0.002 isNeList(__(V1:S,V2:S)) -> U41(isList(V1:S),V2:S) 0.002/0.002 isNeList(__(V1:S,V2:S)) -> U51(isNeList(V1:S),V2:S) 0.002/0.002 isNeList(V:S) -> U31(isQid(V:S)) 0.002/0.002 isNePal(__(I:S,__(P:S,I:S))) -> U71(isQid(I:S),P:S) 0.002/0.002 isNePal(V:S) -> U61(isQid(V:S)) 0.002/0.002 isPal(nil) -> tt 0.002/0.002 isPal(V:S) -> U81(isNePal(V:S)) 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 (U21 1) 0.002/0.002 (U22 1) 0.002/0.002 (U31 1) 0.002/0.002 (U41 1) 0.002/0.002 (U42 1) 0.002/0.002 (U51 1) 0.002/0.002 (U52 1) 0.002/0.002 (U61 1) 0.002/0.002 (U71 1) 0.002/0.002 (U72 1) 0.002/0.002 (U81 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 (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) -> tt 0.002/0.002 U21(tt,V2:S) -> U22(isList(V2:S)) 0.002/0.002 U22(tt) -> tt 0.002/0.002 U31(tt) -> tt 0.002/0.002 U41(tt,V2:S) -> U42(isNeList(V2:S)) 0.002/0.002 U42(tt) -> tt 0.002/0.002 U51(tt,V2:S) -> U52(isList(V2:S)) 0.002/0.002 U52(tt) -> tt 0.002/0.002 U61(tt) -> tt 0.002/0.002 U71(tt,P:S) -> U72(isPal(P:S)) 0.002/0.002 U72(tt) -> tt 0.002/0.002 U81(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(isList(V1:S),V2:S) 0.002/0.002 isList(nil) -> tt 0.002/0.002 isList(V:S) -> U11(isNeList(V:S)) 0.002/0.002 isNeList(__(V1:S,V2:S)) -> U41(isList(V1:S),V2:S) 0.002/0.002 isNeList(__(V1:S,V2:S)) -> U51(isNeList(V1:S),V2:S) 0.002/0.002 isNeList(V:S) -> U31(isQid(V:S)) 0.002/0.002 isNePal(__(I:S,__(P:S,I:S))) -> U71(isQid(I:S),P:S) 0.002/0.002 isNePal(V:S) -> U61(isQid(V:S)) 0.002/0.002 isPal(nil) -> tt 0.002/0.002 isPal(V:S) -> U81(isNePal(V:S)) 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) -> tt 0.002/0.002 U21(tt,V2:S) -> U22(isList(V2:S)) 0.002/0.002 U22(tt) -> tt 0.002/0.002 U31(tt) -> tt 0.002/0.002 U41(tt,V2:S) -> U42(isNeList(V2:S)) 0.002/0.002 U42(tt) -> tt 0.002/0.002 U51(tt,V2:S) -> U52(isList(V2:S)) 0.002/0.002 U52(tt) -> tt 0.002/0.002 U61(tt) -> tt 0.002/0.002 U71(tt,P:S) -> U72(isPal(P:S)) 0.002/0.002 U72(tt) -> tt 0.002/0.002 U81(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(isList(V1:S),V2:S) 0.002/0.002 isList(nil) -> tt 0.002/0.002 isList(V:S) -> U11(isNeList(V:S)) 0.002/0.002 isNeList(__(V1:S,V2:S)) -> U41(isList(V1:S),V2:S) 0.002/0.002 isNeList(__(V1:S,V2:S)) -> U51(isNeList(V1:S),V2:S) 0.002/0.002 isNeList(V:S) -> U31(isQid(V:S)) 0.002/0.002 isNePal(__(I:S,__(P:S,I:S))) -> U71(isQid(I:S),P:S) 0.002/0.002 isNePal(V:S) -> U61(isQid(V:S)) 0.002/0.002 isPal(nil) -> tt 0.002/0.002 isPal(V:S) -> U81(isNePal(V:S)) 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 V2, V2, V2, P, X, Y, Z, X, X, V1, V2, V, V1, V2, V1, V2, V, I, P, V, V 0.002/0.002 -> UVars: 0.002/0.002 (UV-RuleId: 1, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 2, UV-LActive: [], UV-RActive: [], UV-LFrozen: [V2], UV-RFrozen: [V2]) 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: [], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 5, UV-LActive: [], UV-RActive: [], UV-LFrozen: [V2], UV-RFrozen: [V2]) 0.002/0.002 (UV-RuleId: 6, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 7, UV-LActive: [], UV-RActive: [], UV-LFrozen: [V2], UV-RFrozen: [V2]) 0.002/0.002 (UV-RuleId: 8, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 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: [P], UV-RFrozen: [P]) 0.002/0.002 (UV-RuleId: 11, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 12, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 13, UV-LActive: [X, Y, Z], UV-RActive: [X, Y, Z], UV-LFrozen: [], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 14, UV-LActive: [X], UV-RActive: [X], UV-LFrozen: [], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 15, UV-LActive: [X], UV-RActive: [X], UV-LFrozen: [], UV-RFrozen: []) 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: [], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 18, UV-LActive: [], UV-RActive: [], UV-LFrozen: [V], UV-RFrozen: [V]) 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: [V], UV-RFrozen: [V]) 0.002/0.002 (UV-RuleId: 22, UV-LActive: [], UV-RActive: [], UV-LFrozen: [I, P], UV-RFrozen: [I, P]) 0.002/0.002 (UV-RuleId: 23, UV-LActive: [], UV-RActive: [], UV-LFrozen: [V], UV-RFrozen: [V]) 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: [], UV-RFrozen: []) 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: [], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 29, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 30, 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 0.002/0.002 -> PVars: 0.002/0.002 V2: [x9, x10, x11, x19, x22, x24], P: [x12, x27], X: [x13, x16, x17], Y: [x14], Z: [x15], V1: [x18, x21, x23], V: [x20, x25, x28, x29], I: [x26] 0.002/0.002 0.002/0.002 -> Rlps: 0.002/0.002 (rule: U11(tt) -> tt, id: 1, possubterms: U11(tt)->[], tt->[1]) 0.002/0.002 (rule: U21(tt,x9:S) -> U22(isList(x9:S)), id: 2, possubterms: U21(tt,x9:S)->[], tt->[1]) 0.002/0.002 (rule: U22(tt) -> tt, id: 3, possubterms: U22(tt)->[], tt->[1]) 0.002/0.002 (rule: U31(tt) -> tt, id: 4, possubterms: U31(tt)->[], tt->[1]) 0.002/0.002 (rule: U41(tt,x10:S) -> U42(isNeList(x10:S)), id: 5, possubterms: U41(tt,x10:S)->[], tt->[1]) 0.002/0.002 (rule: U42(tt) -> tt, id: 6, possubterms: U42(tt)->[], tt->[1]) 0.002/0.002 (rule: U51(tt,x11:S) -> U52(isList(x11:S)), id: 7, possubterms: U51(tt,x11:S)->[], tt->[1]) 0.002/0.002 (rule: U52(tt) -> tt, id: 8, possubterms: U52(tt)->[], tt->[1]) 0.002/0.002 (rule: U61(tt) -> tt, id: 9, possubterms: U61(tt)->[], tt->[1]) 0.002/0.002 (rule: U71(tt,x12:S) -> U72(isPal(x12:S)), id: 10, possubterms: U71(tt,x12:S)->[], tt->[1]) 0.002/0.002 (rule: U72(tt) -> tt, id: 11, possubterms: U72(tt)->[], tt->[1]) 0.002/0.002 (rule: U81(tt) -> tt, id: 12, possubterms: U81(tt)->[], tt->[1]) 0.002/0.002 (rule: __(__(x13:S,x14:S),x15:S) -> __(x13:S,__(x14:S,x15:S)), id: 13, possubterms: __(__(x13:S,x14:S),x15:S)->[], __(x13:S,x14:S)->[1]) 0.002/0.002 (rule: __(nil,x16:S) -> x16:S, id: 14, possubterms: __(nil,x16:S)->[], nil->[1]) 0.002/0.002 (rule: __(x17:S,nil) -> x17:S, id: 15, possubterms: __(x17:S,nil)->[], nil->[2]) 0.002/0.002 (rule: isList(__(x18:S,x19:S)) -> U21(isList(x18:S),x19:S), id: 16, possubterms: isList(__(x18:S,x19:S))->[]) 0.002/0.002 (rule: isList(nil) -> tt, id: 17, possubterms: isList(nil)->[]) 0.002/0.002 (rule: isList(x20:S) -> U11(isNeList(x20:S)), id: 18, possubterms: isList(x20:S)->[]) 0.002/0.002 (rule: isNeList(__(x21:S,x22:S)) -> U41(isList(x21:S),x22:S), id: 19, possubterms: isNeList(__(x21:S,x22:S))->[]) 0.002/0.002 (rule: isNeList(__(x23:S,x24:S)) -> U51(isNeList(x23:S),x24:S), id: 20, possubterms: isNeList(__(x23:S,x24:S))->[]) 0.002/0.002 (rule: isNeList(x25:S) -> U31(isQid(x25:S)), id: 21, possubterms: isNeList(x25:S)->[]) 0.002/0.002 (rule: isNePal(__(x26:S,__(x27:S,x26:S))) -> U71(isQid(x26:S),x27:S), id: 22, possubterms: isNePal(__(x26:S,__(x27:S,x26:S)))->[]) 0.002/0.002 (rule: isNePal(x28:S) -> U61(isQid(x28:S)), id: 23, possubterms: isNePal(x28:S)->[]) 0.002/0.002 (rule: isPal(nil) -> tt, id: 24, possubterms: isPal(nil)->[]) 0.002/0.002 (rule: isPal(x29:S) -> U81(isNePal(x29:S)), id: 25, possubterms: isPal(x29:S)->[]) 0.002/0.002 (rule: isQid(a) -> tt, id: 26, possubterms: isQid(a)->[]) 0.002/0.002 (rule: isQid(e) -> tt, id: 27, possubterms: isQid(e)->[]) 0.002/0.002 (rule: isQid(i) -> tt, id: 28, possubterms: isQid(i)->[]) 0.002/0.002 (rule: isQid(o) -> tt, id: 29, possubterms: isQid(o)->[]) 0.002/0.002 (rule: isQid(u) -> tt, id: 30, possubterms: isQid(u)->[]) 0.002/0.002 0.002/0.002 -> Unifications: 0.002/0.002 (R13 unifies with R13 at p: [1], l: __(__(x13:S,x14:S),x15:S), lp: __(x13:S,x14:S), sig: {x13:S -> __(X:S,Y:S),x14:S -> Z:S}, l': __(__(X:S,Y:S),Z:S), r: __(x13:S,__(x14:S,x15:S)), r': __(X:S,__(Y:S,Z:S))) 0.002/0.002 (R13 unifies with R14 at p: [1], l: __(__(x13:S,x14:S),x15:S), lp: __(x13:S,x14:S), sig: {x13:S -> nil,x14:S -> X:S}, l': __(nil,X:S), r: __(x13:S,__(x14:S,x15:S)), r': X:S) 0.002/0.002 (R13 unifies with R15 at p: [1], l: __(__(x13:S,x14:S),x15:S), lp: __(x13:S,x14:S), sig: {x13:S -> X:S,x14:S -> nil}, l': __(X:S,nil), r: __(x13:S,__(x14:S,x15:S)), r': X:S) 0.002/0.002 (R15 unifies with R13 at p: [], l: __(x17:S,nil), lp: __(x17:S,nil), sig: {Z:S -> nil,x17:S -> __(X:S,Y:S)}, l': __(__(X:S,Y:S),Z:S), r: x17:S, r': __(X:S,__(Y:S,Z:S))) 0.002/0.002 (R15 unifies with R14 at p: [], l: __(x17:S,nil), lp: __(x17:S,nil), sig: {X:S -> nil,x17:S -> nil}, l': __(nil,X:S), r: x17:S, r': X:S) 0.002/0.002 (R18 unifies with R16 at p: [], l: isList(x20:S), lp: isList(x20:S), sig: {x20:S -> __(V1:S,V2:S)}, l': isList(__(V1:S,V2:S)), r: U11(isNeList(x20:S)), r': U21(isList(V1:S),V2:S)) 0.002/0.002 (R18 unifies with R17 at p: [], l: isList(x20:S), lp: isList(x20:S), sig: {x20:S -> nil}, l': isList(nil), r: U11(isNeList(x20:S)), r': tt) 0.002/0.002 (R20 unifies with R19 at p: [], l: isNeList(__(x23:S,x24:S)), lp: isNeList(__(x23:S,x24:S)), sig: {x23:S -> V1:S,x24:S -> V2:S}, l': isNeList(__(V1:S,V2:S)), r: U51(isNeList(x23:S),x24:S), r': U41(isList(V1:S),V2:S)) 0.002/0.002 (R21 unifies with R19 at p: [], l: isNeList(x25:S), lp: isNeList(x25:S), sig: {x25:S -> __(V1:S,V2:S)}, l': isNeList(__(V1:S,V2:S)), r: U31(isQid(x25:S)), r': U41(isList(V1:S),V2:S)) 0.002/0.002 (R21 unifies with R20 at p: [], l: isNeList(x25:S), lp: isNeList(x25:S), sig: {x25:S -> __(V1:S,V2:S)}, l': isNeList(__(V1:S,V2:S)), r: U31(isQid(x25:S)), r': U51(isNeList(V1:S),V2:S)) 0.002/0.002 (R23 unifies with R22 at p: [], l: isNePal(x28:S), lp: isNePal(x28:S), sig: {x28:S -> __(I:S,__(P:S,I:S))}, l': isNePal(__(I:S,__(P:S,I:S))), r: U61(isQid(x28:S)), r': U71(isQid(I:S),P:S)) 0.002/0.002 (R25 unifies with R24 at p: [], l: isPal(x29:S), lp: isPal(x29:S), sig: {x29:S -> nil}, l': isPal(nil), r: U81(isNePal(x29: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 => Not trivial, Overlay, NW0, N2 0.002/0.002 <__(X:S,Z:S),__(nil,__(X:S,Z:S))> => Not trivial, Not overlay, NW0, N3 0.002/0.002 <__(X:S,__(Y:S,nil)),__(X:S,Y:S)> => Not trivial, Overlay, NW0, N4 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, N5 0.002/0.002 => Trivial, Overlay, NW0, N6 0.002/0.002 => Not trivial, Overlay, NW0, N7 0.002/0.002 => Not trivial, Overlay, NW0, N8 0.002/0.002 => Not trivial, Overlay, NW0, N9 0.002/0.002 <__(X:S,Z:S),__(X:S,__(nil,Z:S))> => Not trivial, Not 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, 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: U21(isList(V1:S),V2:S) 0.002/0.002 Nodes: [0,1,2] 0.002/0.002 Edges: [(0,1),(1,2)] 0.002/0.002 ID: 0 => ('U21(isList(V1:S),V2:S)', D0) 0.002/0.002 ID: 1 => ('U21(U11(isNeList(V1:S)),V2:S)', D1, R18, P[1], S{x20:S -> V1:S}), NR: 'U11(isNeList(V1:S))' 0.002/0.002 ID: 2 => ('U21(U11(U31(isQid(V1:S))),V2:S)', D2, R21, P[1, 1], S{x25:S -> V1:S}), NR: 'U31(isQid(V1:S))' 0.002/0.002 t: U11(isNeList(__(V1:S,V2:S))) 0.002/0.002 Nodes: [0,1,2,3,4,5,6] 0.002/0.002 Edges: [(0,1),(0,2),(0,3),(1,4),(2,5),(4,6)] 0.002/0.002 ID: 0 => ('U11(isNeList(__(V1:S,V2:S)))', D0) 0.002/0.002 ID: 1 => ('U11(U41(isList(V1:S),V2:S))', D1, R19, P[1], S{x21:S -> V1:S, x22:S -> V2:S}), NR: 'U41(isList(V1:S),V2:S)' 0.002/0.002 ID: 2 => ('U11(U51(isNeList(V1:S),V2:S))', D1, R20, P[1], S{x23:S -> V1:S, x24:S -> V2:S}), NR: 'U51(isNeList(V1:S),V2:S)' 0.002/0.002 ID: 3 => ('U11(U31(isQid(__(V1:S,V2:S))))', D1, R21, P[1], S{x25:S -> __(V1:S,V2:S)}), NR: 'U31(isQid(__(V1:S,V2:S)))' 0.002/0.002 ID: 4 => ('U11(U41(U11(isNeList(V1:S)),V2:S))', D2, R18, P[1, 1], S{x20:S -> V1:S}), NR: 'U11(isNeList(V1:S))' 0.002/0.002 ID: 5 => ('U11(U51(U31(isQid(V1:S)),V2:S))', D2, R21, P[1, 1], S{x25:S -> V1:S}), NR: 'U31(isQid(V1:S))' 0.002/0.002 ID: 6 => ('U11(U41(U11(U31(isQid(V1:S))),V2:S))', D3, R21, P[1, 1, 1], S{x25:S -> V1:S}), NR: 'U31(isQid(V1:S))' 0.002/0.002 U21(isList(V1:S),V2:S) ->* no union *<- U11(isNeList(__(V1:S,V2: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.01user 0.00system 0:00.02elapsed 69%CPU (0avgtext+0avgdata 11944maxresident)k 0.002/0.002 0inputs+0outputs (0major+1156minor)pagefaults 0swaps