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 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.002/0.002 (STRATEGY CONTEXTSENSITIVE 0.002/0.002 (__ 1 2) 0.002/0.002 (and 1) 0.002/0.002 (isList 1) 0.002/0.002 (isNeList 1) 0.002/0.002 (isNePal 1) 0.002/0.002 (isPal 1) 0.002/0.002 (isQid 1) 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 __(__(X:S:S,Y:S:S),Z:S:S) -> __(X:S:S,__(Y:S:S,Z:S:S)) 0.002/0.002 __(nil,X:S:S) -> X:S:S 0.002/0.002 __(X:S:S,nil) -> X:S:S 0.002/0.002 and(tt,X:S:S) -> X:S:S 0.002/0.002 isList(__(V1:S:S,V2:S:S)) -> and(isList(V1:S:S),isList(V2:S:S)) 0.002/0.002 isList(nil) -> tt 0.002/0.002 isList(V:S:S) -> isNeList(V:S:S) 0.002/0.002 isNeList(__(V1:S:S,V2:S:S)) -> and(isList(V1:S:S),isNeList(V2:S:S)) 0.002/0.002 isNeList(__(V1:S:S,V2:S:S)) -> and(isNeList(V1:S:S),isList(V2:S:S)) 0.002/0.002 isNeList(V:S:S) -> isQid(V:S:S) 0.002/0.002 isNePal(__(I:S:S,__(P:S:S,I:S:S))) -> and(isQid(I:S:S),isPal(P:S:S)) 0.002/0.002 isNePal(V:S:S) -> isQid(V:S:S) 0.002/0.002 isPal(nil) -> tt 0.002/0.002 isPal(V:S:S) -> isNePal(V:S: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 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.002/0.002 (STRATEGY CONTEXTSENSITIVE 0.002/0.002 (__ 1 2) 0.002/0.002 (and 1) 0.002/0.002 (isList 1) 0.002/0.002 (isNeList 1) 0.002/0.002 (isNePal 1) 0.002/0.002 (isPal 1) 0.002/0.002 (isQid 1) 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 __(__(X:S:S,Y:S:S),Z:S:S) -> __(X:S:S,__(Y:S:S,Z:S:S)) 0.002/0.002 __(nil,X:S:S) -> X:S:S 0.002/0.002 __(X:S:S,nil) -> X:S:S 0.002/0.002 and(tt,X:S:S) -> X:S:S 0.002/0.002 isList(__(V1:S:S,V2:S:S)) -> and(isList(V1:S:S),isList(V2:S:S)) 0.002/0.002 isList(nil) -> tt 0.002/0.002 isList(V:S:S) -> isNeList(V:S:S) 0.002/0.002 isNeList(__(V1:S:S,V2:S:S)) -> and(isList(V1:S:S),isNeList(V2:S:S)) 0.002/0.002 isNeList(__(V1:S:S,V2:S:S)) -> and(isNeList(V1:S:S),isList(V2:S:S)) 0.002/0.002 isNeList(V:S:S) -> isQid(V:S:S) 0.002/0.002 isNePal(__(I:S:S,__(P:S:S,I:S:S))) -> and(isQid(I:S:S),isPal(P:S:S)) 0.002/0.002 isNePal(V:S:S) -> isQid(V:S:S) 0.002/0.002 isPal(nil) -> tt 0.002/0.002 isPal(V:S:S) -> isNePal(V:S: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 CS-TRS Processor: 0.002/0.002 R is a CS-TRS 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 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.002/0.002 (STRATEGY CONTEXTSENSITIVE 0.002/0.002 (__ 1 2) 0.002/0.002 (and 1) 0.002/0.002 (isList 1) 0.002/0.002 (isNeList 1) 0.002/0.002 (isNePal 1) 0.002/0.002 (isPal 1) 0.002/0.002 (isQid 1) 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 __(__(X:S:S,Y:S:S),Z:S:S) -> __(X:S:S,__(Y:S:S,Z:S:S)) 0.002/0.002 __(nil,X:S:S) -> X:S:S 0.002/0.002 __(X:S:S,nil) -> X:S:S 0.002/0.002 and(tt,X:S:S) -> X:S:S 0.002/0.002 isList(__(V1:S:S,V2:S:S)) -> and(isList(V1:S:S),isList(V2:S:S)) 0.002/0.002 isList(nil) -> tt 0.002/0.002 isList(V:S:S) -> isNeList(V:S:S) 0.002/0.002 isNeList(__(V1:S:S,V2:S:S)) -> and(isList(V1:S:S),isNeList(V2:S:S)) 0.002/0.002 isNeList(__(V1:S:S,V2:S:S)) -> and(isNeList(V1:S:S),isList(V2:S:S)) 0.002/0.002 isNeList(V:S:S) -> isQid(V:S:S) 0.002/0.002 isNePal(__(I:S:S,__(P:S:S,I:S:S))) -> and(isQid(I:S:S),isPal(P:S:S)) 0.002/0.002 isNePal(V:S:S) -> isQid(V:S:S) 0.002/0.002 isPal(nil) -> tt 0.002/0.002 isPal(V:S:S) -> isNePal(V:S: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 __(__(X:S:S,Y:S:S),Z:S:S) -> __(X:S:S,__(Y:S:S,Z:S:S)) 0.002/0.002 __(nil,X:S:S) -> X:S:S 0.002/0.002 __(X:S:S,nil) -> X:S:S 0.002/0.002 and(tt,X:S:S) -> X:S:S 0.002/0.002 isList(__(V1:S:S,V2:S:S)) -> and(isList(V1:S:S),isList(V2:S:S)) 0.002/0.002 isList(nil) -> tt 0.002/0.002 isList(V:S:S) -> isNeList(V:S:S) 0.002/0.002 isNeList(__(V1:S:S,V2:S:S)) -> and(isList(V1:S:S),isNeList(V2:S:S)) 0.002/0.002 isNeList(__(V1:S:S,V2:S:S)) -> and(isNeList(V1:S:S),isList(V2:S:S)) 0.002/0.002 isNeList(V:S:S) -> isQid(V:S:S) 0.002/0.002 isNePal(__(I:S:S,__(P:S:S,I:S:S))) -> and(isQid(I:S:S),isPal(P:S:S)) 0.002/0.002 isNePal(V:S:S) -> isQid(V:S:S) 0.002/0.002 isPal(nil) -> tt 0.002/0.002 isPal(V:S:S) -> isNePal(V:S: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 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 0.002/0.002 -> UVars: 0.002/0.002 (UV-RuleId: 1, UV-LActive: [X:S, Y:S, Z:S], UV-RActive: [X:S, Y:S, Z:S], UV-LFrozen: [], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 2, UV-LActive: [X:S], UV-RActive: [X:S], UV-LFrozen: [], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 3, UV-LActive: [X:S], UV-RActive: [X:S], UV-LFrozen: [], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 4, UV-LActive: [], UV-RActive: [X:S], UV-LFrozen: [X:S], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 5, UV-LActive: [V1:S, V2:S], UV-RActive: [V1:S], UV-LFrozen: [], UV-RFrozen: [V2:S]) 0.002/0.002 (UV-RuleId: 6, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 7, UV-LActive: [V:S], UV-RActive: [V:S], UV-LFrozen: [], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 8, UV-LActive: [V1:S, V2:S], UV-RActive: [V1:S], UV-LFrozen: [], UV-RFrozen: [V2:S]) 0.002/0.002 (UV-RuleId: 9, UV-LActive: [V1:S, V2:S], UV-RActive: [V1:S], UV-LFrozen: [], UV-RFrozen: [V2:S]) 0.002/0.002 (UV-RuleId: 10, UV-LActive: [V:S], UV-RActive: [V:S], UV-LFrozen: [], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 11, UV-LActive: [I:S, P:S], UV-RActive: [I:S], UV-LFrozen: [], UV-RFrozen: [P:S]) 0.002/0.002 (UV-RuleId: 12, UV-LActive: [V:S], UV-RActive: [V:S], UV-LFrozen: [], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 13, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 14, UV-LActive: [V:S], UV-RActive: [V:S], UV-LFrozen: [], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 15, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 16, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 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: [], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 19, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.002/0.002 -> FVars: 0.002/0.002 x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23, x24, x25, x26, x27 0.002/0.002 -> PVars: 0.002/0.002 X:S: [x10, x13, x14, x15], Y:S: [x11], Z:S: [x12], V1:S: [x16, x19, x21], V2:S: [x17, x20, x22], V:S: [x18, x23, x26, x27], I:S: [x24], P:S: [x25] 0.002/0.002 0.002/0.002 -> Rlps: 0.002/0.002 (rule: __(__(x10:S,x11:S),x12:S) -> __(x10:S,__(x11:S,x12:S)), id: 1, possubterms: __(__(x10:S,x11:S),x12:S)->[], __(x10:S,x11:S)->[1]) 0.002/0.002 (rule: __(nil,x13:S) -> x13:S, id: 2, possubterms: __(nil,x13:S)->[], nil->[1]) 0.002/0.002 (rule: __(x14:S,nil) -> x14:S, id: 3, possubterms: __(x14:S,nil)->[], nil->[2]) 0.002/0.002 (rule: and(tt,x15:S) -> x15:S, id: 4, possubterms: and(tt,x15:S)->[], tt->[1]) 0.002/0.002 (rule: isList(__(x16:S,x17:S)) -> and(isList(x16:S),isList(x17:S)), id: 5, possubterms: isList(__(x16:S,x17:S))->[], __(x16:S,x17:S)->[1]) 0.002/0.002 (rule: isList(nil) -> tt, id: 6, possubterms: isList(nil)->[], nil->[1]) 0.002/0.002 (rule: isList(x18:S) -> isNeList(x18:S), id: 7, possubterms: isList(x18:S)->[]) 0.002/0.002 (rule: isNeList(__(x19:S,x20:S)) -> and(isList(x19:S),isNeList(x20:S)), id: 8, possubterms: isNeList(__(x19:S,x20:S))->[], __(x19:S,x20:S)->[1]) 0.002/0.002 (rule: isNeList(__(x21:S,x22:S)) -> and(isNeList(x21:S),isList(x22:S)), id: 9, possubterms: isNeList(__(x21:S,x22:S))->[], __(x21:S,x22:S)->[1]) 0.002/0.002 (rule: isNeList(x23:S) -> isQid(x23:S), id: 10, possubterms: isNeList(x23:S)->[]) 0.002/0.002 (rule: isNePal(__(x24:S,__(x25:S,x24:S))) -> and(isQid(x24:S),isPal(x25:S)), id: 11, possubterms: isNePal(__(x24:S,__(x25:S,x24:S)))->[], __(x24:S,__(x25:S,x24:S))->[1], __(x25:S,x24:S)->[1, 2]) 0.002/0.002 (rule: isNePal(x26:S) -> isQid(x26:S), id: 12, possubterms: isNePal(x26:S)->[]) 0.002/0.002 (rule: isPal(nil) -> tt, id: 13, possubterms: isPal(nil)->[], nil->[1]) 0.002/0.002 (rule: isPal(x27:S) -> isNePal(x27:S), id: 14, possubterms: isPal(x27:S)->[]) 0.002/0.002 (rule: isQid(a) -> tt, id: 15, possubterms: isQid(a)->[], a->[1]) 0.002/0.002 (rule: isQid(e) -> tt, id: 16, possubterms: isQid(e)->[], e->[1]) 0.002/0.002 (rule: isQid(i) -> tt, id: 17, possubterms: isQid(i)->[], i->[1]) 0.002/0.002 (rule: isQid(o) -> tt, id: 18, possubterms: isQid(o)->[], o->[1]) 0.002/0.002 (rule: isQid(u) -> tt, id: 19, possubterms: isQid(u)->[], u->[1]) 0.002/0.002 0.002/0.002 -> Unifications: 0.002/0.002 (R1 unifies with R1 at p: [1], l: __(__(x10:S,x11:S),x12:S), lp: __(x10:S,x11:S), sig: {x10:S -> __(X:S:S,Y:S:S),x11:S -> Z:S:S}, l': __(__(X:S:S,Y:S:S),Z:S:S), r: __(x10:S,__(x11:S,x12:S)), r': __(X:S:S,__(Y:S:S,Z:S:S))) 0.002/0.002 (R1 unifies with R2 at p: [1], l: __(__(x10:S,x11:S),x12:S), lp: __(x10:S,x11:S), sig: {x10:S -> nil,x11:S -> X:S:S}, l': __(nil,X:S:S), r: __(x10:S,__(x11:S,x12:S)), r': X:S:S) 0.002/0.002 (R1 unifies with R3 at p: [1], l: __(__(x10:S,x11:S),x12:S), lp: __(x10:S,x11:S), sig: {x10:S -> X:S:S,x11:S -> nil}, l': __(X:S:S,nil), r: __(x10:S,__(x11:S,x12:S)), r': X:S:S) 0.002/0.002 (R3 unifies with R1 at p: [], l: __(x14:S,nil), lp: __(x14:S,nil), sig: {Z:S:S -> nil,x14:S -> __(X:S:S,Y:S:S)}, l': __(__(X:S:S,Y:S:S),Z:S:S), r: x14:S, r': __(X:S:S,__(Y:S:S,Z:S:S))) 0.002/0.002 (R3 unifies with R2 at p: [], l: __(x14:S,nil), lp: __(x14:S,nil), sig: {X:S:S -> nil,x14:S -> nil}, l': __(nil,X:S:S), r: x14:S, r': X:S:S) 0.002/0.002 (R5 unifies with R1 at p: [1], l: isList(__(x16:S,x17:S)), lp: __(x16:S,x17:S), sig: {x16:S -> __(X:S:S,Y:S:S),x17:S -> Z:S:S}, l': __(__(X:S:S,Y:S:S),Z:S:S), r: and(isList(x16:S),isList(x17:S)), r': __(X:S:S,__(Y:S:S,Z:S:S))) 0.002/0.002 (R5 unifies with R2 at p: [1], l: isList(__(x16:S,x17:S)), lp: __(x16:S,x17:S), sig: {x16:S -> nil,x17:S -> X:S:S}, l': __(nil,X:S:S), r: and(isList(x16:S),isList(x17:S)), r': X:S:S) 0.002/0.002 (R5 unifies with R3 at p: [1], l: isList(__(x16:S,x17:S)), lp: __(x16:S,x17:S), sig: {x16:S -> X:S:S,x17:S -> nil}, l': __(X:S:S,nil), r: and(isList(x16:S),isList(x17:S)), r': X:S:S) 0.002/0.002 (R7 unifies with R5 at p: [], l: isList(x18:S), lp: isList(x18:S), sig: {x18:S -> __(V1:S:S,V2:S:S)}, l': isList(__(V1:S:S,V2:S:S)), r: isNeList(x18:S), r': and(isList(V1:S:S),isList(V2:S:S))) 0.002/0.002 (R7 unifies with R6 at p: [], l: isList(x18:S), lp: isList(x18:S), sig: {x18:S -> nil}, l': isList(nil), r: isNeList(x18:S), r': tt) 0.002/0.002 (R8 unifies with R1 at p: [1], l: isNeList(__(x19:S,x20:S)), lp: __(x19:S,x20:S), sig: {x19:S -> __(X:S:S,Y:S:S),x20:S -> Z:S:S}, l': __(__(X:S:S,Y:S:S),Z:S:S), r: and(isList(x19:S),isNeList(x20:S)), r': __(X:S:S,__(Y:S:S,Z:S:S))) 0.002/0.002 (R8 unifies with R2 at p: [1], l: isNeList(__(x19:S,x20:S)), lp: __(x19:S,x20:S), sig: {x19:S -> nil,x20:S -> X:S:S}, l': __(nil,X:S:S), r: and(isList(x19:S),isNeList(x20:S)), r': X:S:S) 0.002/0.002 (R8 unifies with R3 at p: [1], l: isNeList(__(x19:S,x20:S)), lp: __(x19:S,x20:S), sig: {x19:S -> X:S:S,x20:S -> nil}, l': __(X:S:S,nil), r: and(isList(x19:S),isNeList(x20:S)), r': X:S:S) 0.002/0.002 (R9 unifies with R8 at p: [], l: isNeList(__(x21:S,x22:S)), lp: isNeList(__(x21:S,x22:S)), sig: {x21:S -> V1:S:S,x22:S -> V2:S:S}, l': isNeList(__(V1:S:S,V2:S:S)), r: and(isNeList(x21:S),isList(x22:S)), r': and(isList(V1:S:S),isNeList(V2:S:S))) 0.002/0.002 (R9 unifies with R1 at p: [1], l: isNeList(__(x21:S,x22:S)), lp: __(x21:S,x22:S), sig: {x21:S -> __(X:S:S,Y:S:S),x22:S -> Z:S:S}, l': __(__(X:S:S,Y:S:S),Z:S:S), r: and(isNeList(x21:S),isList(x22:S)), r': __(X:S:S,__(Y:S:S,Z:S:S))) 0.002/0.002 (R9 unifies with R2 at p: [1], l: isNeList(__(x21:S,x22:S)), lp: __(x21:S,x22:S), sig: {x21:S -> nil,x22:S -> X:S:S}, l': __(nil,X:S:S), r: and(isNeList(x21:S),isList(x22:S)), r': X:S:S) 0.002/0.002 (R9 unifies with R3 at p: [1], l: isNeList(__(x21:S,x22:S)), lp: __(x21:S,x22:S), sig: {x21:S -> X:S:S,x22:S -> nil}, l': __(X:S:S,nil), r: and(isNeList(x21:S),isList(x22:S)), r': X:S:S) 0.002/0.002 (R10 unifies with R8 at p: [], l: isNeList(x23:S), lp: isNeList(x23:S), sig: {x23:S -> __(V1:S:S,V2:S:S)}, l': isNeList(__(V1:S:S,V2:S:S)), r: isQid(x23:S), r': and(isList(V1:S:S),isNeList(V2:S:S))) 0.002/0.002 (R10 unifies with R9 at p: [], l: isNeList(x23:S), lp: isNeList(x23:S), sig: {x23:S -> __(V1:S:S,V2:S:S)}, l': isNeList(__(V1:S:S,V2:S:S)), r: isQid(x23:S), r': and(isNeList(V1:S:S),isList(V2:S:S))) 0.002/0.002 (R11 unifies with R1 at p: [1], l: isNePal(__(x24:S,__(x25:S,x24:S))), lp: __(x24:S,__(x25:S,x24:S)), sig: {Z:S:S -> __(x25:S,__(X:S:S,Y:S:S)),x24:S -> __(X:S:S,Y:S:S)}, l': __(__(X:S:S,Y:S:S),Z:S:S), r: and(isQid(x24:S),isPal(x25:S)), r': __(X:S:S,__(Y:S:S,Z:S:S))) 0.002/0.002 (R11 unifies with R2 at p: [1], l: isNePal(__(x24:S,__(x25:S,x24:S))), lp: __(x24:S,__(x25:S,x24:S)), sig: {X:S:S -> __(x25:S,nil),x24:S -> nil}, l': __(nil,X:S:S), r: and(isQid(x24:S),isPal(x25:S)), r': X:S:S) 0.002/0.002 (R11 unifies with R1 at p: [1,2], l: isNePal(__(x24:S,__(x25:S,x24:S))), lp: __(x25:S,x24:S), sig: {x24:S -> Z:S:S,x25:S -> __(X:S:S,Y:S:S)}, l': __(__(X:S:S,Y:S:S),Z:S:S), r: and(isQid(x24:S),isPal(x25:S)), r': __(X:S:S,__(Y:S:S,Z:S:S))) 0.002/0.002 (R11 unifies with R2 at p: [1,2], l: isNePal(__(x24:S,__(x25:S,x24:S))), lp: __(x25:S,x24:S), sig: {x24:S -> X:S:S,x25:S -> nil}, l': __(nil,X:S:S), r: and(isQid(x24:S),isPal(x25:S)), r': X:S:S) 0.002/0.002 (R11 unifies with R3 at p: [1,2], l: isNePal(__(x24:S,__(x25:S,x24:S))), lp: __(x25:S,x24:S), sig: {x24:S -> nil,x25:S -> X:S:S}, l': __(X:S:S,nil), r: and(isQid(x24:S),isPal(x25:S)), r': X:S:S) 0.002/0.002 (R12 unifies with R11 at p: [], l: isNePal(x26:S), lp: isNePal(x26:S), sig: {x26:S -> __(I:S:S,__(P:S:S,I:S:S))}, l': isNePal(__(I:S:S,__(P:S:S,I:S:S))), r: isQid(x26:S), r': and(isQid(I:S:S),isPal(P:S:S))) 0.002/0.002 (R14 unifies with R13 at p: [], l: isPal(x27:S), lp: isPal(x27:S), sig: {x27:S -> nil}, l': isPal(nil), r: isNePal(x27:S), r': tt) 0.002/0.002 0.002/0.002 -> Critical pairs info: 0.002/0.002 <__(X:S:S,__(Y:S:S,nil)),__(X:S:S,Y:S:S)> => Not trivial, Overlay, NW0, N1 0.002/0.002 => Not trivial, Overlay, NW0, N2 0.002/0.002 <__(X:S:S,Z:S:S),__(nil,__(X:S:S,Z:S:S))> => Not trivial, Not overlay, NW0, N3 0.002/0.002 => Not trivial, Not overlay, NW0, N4 0.002/0.002 => Not trivial, Overlay, NW0, N5 0.002/0.002 => Not trivial, Overlay, NW0, N6 0.002/0.002 => Not trivial, Overlay, NW0, N7 0.002/0.002 => Not trivial, Not overlay, NW0, N8 0.002/0.002 => Not trivial, Not overlay, NW0, N9 0.002/0.002 => Not trivial, Not overlay, NW0, N10 0.002/0.002 => Not trivial, Not overlay, NW0, N11 0.002/0.002 => Trivial, Overlay, NW0, N12 0.002/0.002 => Not trivial, Overlay, NW0, N13 0.002/0.002 => Not trivial, Not overlay, NW0, N14 0.002/0.002 => Not trivial, Not overlay, NW0, N15 0.002/0.002 => Not trivial, Overlay, NW0, N16 0.002/0.002 => Not trivial, Not overlay, NW0, N17 0.002/0.002 <__(__(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, N18 0.002/0.002 => Not trivial, Overlay, NW0, N19 0.002/0.002 => Not trivial, Not overlay, NW0, N20 0.002/0.002 => Not trivial, Not overlay, NW0, N21 0.002/0.002 => Not trivial, Not overlay, NW0, N22 0.002/0.002 => Not trivial, Not overlay, NW0, N23 0.002/0.002 => Not trivial, Not overlay, NW0, N24 0.002/0.002 <__(X:S:S,Z:S:S),__(X:S:S,__(nil,Z:S:S))> => Not trivial, Not overlay, NW0, N25 0.002/0.002 => Not trivial, Not overlay, NW0, N26 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, Not 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: and(isList(V1:S:S),isNeList(V2:S:S)) 0.002/0.002 Nodes: [0,1,2] 0.002/0.002 Edges: [(0,1),(1,2)] 0.002/0.002 ID: 0 => ('and(isList(V1:S:S),isNeList(V2:S:S))', D0) 0.002/0.002 ID: 1 => ('and(isNeList(V1:S:S),isNeList(V2:S:S))', D1, R7, P[1], S{x18:S -> V1:S:S}), NR: 'isNeList(V1:S:S)' 0.002/0.002 ID: 2 => ('and(isQid(V1:S:S),isNeList(V2:S:S))', D2, R10, P[1], S{x23:S -> V1:S:S}), NR: 'isQid(V1:S:S)' 0.002/0.002 t: and(isNeList(V1:S:S),isList(V2:S:S)) 0.002/0.002 Nodes: [0,1] 0.002/0.002 Edges: [(0,1)] 0.002/0.002 ID: 0 => ('and(isNeList(V1:S:S),isList(V2:S:S))', D0) 0.002/0.002 ID: 1 => ('and(isQid(V1:S:S),isList(V2:S:S))', D1, R10, P[1], S{x23:S -> V1:S:S}), NR: 'isQid(V1:S:S)' 0.002/0.002 and(isList(V1:S:S),isNeList(V2:S:S)) ->* no union *<- and(isNeList(V1:S:S),isList(V2:S: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.00system 0:00.02elapsed 57%CPU (0avgtext+0avgdata 11348maxresident)k 0.002/0.002 8inputs+0outputs (0major+1131minor)pagefaults 0swaps