0.001/0.001 NO 0.001/0.001 0.001/0.001 Problem 1: 0.001/0.001 0.001/0.001 0.001/0.001 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.001/0.001 Confluence Problem: 0.001/0.001 (VAR vNonEmpty:S I:S P:S V:S V1:S V2:S X:S Y:S Z:S) 0.001/0.001 (STRATEGY CONTEXTSENSITIVE 0.001/0.001 (__ 1 2) 0.001/0.001 (and 1) 0.001/0.001 (isList) 0.001/0.001 (isNeList) 0.001/0.001 (isNePal) 0.001/0.001 (isPal) 0.001/0.001 (isQid) 0.001/0.001 (a) 0.001/0.001 (e) 0.001/0.001 (fSNonEmpty) 0.001/0.001 (i) 0.001/0.001 (nil) 0.001/0.001 (o) 0.001/0.001 (tt) 0.001/0.001 (u) 0.001/0.001 ) 0.001/0.001 (RULES 0.001/0.001 __(__(X:S,Y:S),Z:S) -> __(X:S,__(Y:S,Z:S)) 0.001/0.001 __(nil,X:S) -> X:S 0.001/0.001 __(X:S,nil) -> X:S 0.001/0.001 and(tt,X:S) -> X:S 0.001/0.001 isList(__(V1:S,V2:S)) -> and(isList(V1:S),isList(V2:S)) 0.001/0.001 isList(nil) -> tt 0.001/0.001 isList(V:S) -> isNeList(V:S) 0.001/0.001 isNeList(__(V1:S,V2:S)) -> and(isList(V1:S),isNeList(V2:S)) 0.001/0.001 isNeList(__(V1:S,V2:S)) -> and(isNeList(V1:S),isList(V2:S)) 0.001/0.001 isNeList(V:S) -> isQid(V:S) 0.001/0.001 isNePal(__(I:S,__(P:S,I:S))) -> and(isQid(I:S),isPal(P:S)) 0.001/0.001 isNePal(V:S) -> isQid(V:S) 0.001/0.001 isPal(nil) -> tt 0.001/0.001 isPal(V:S) -> isNePal(V:S) 0.001/0.001 isQid(a) -> tt 0.001/0.001 isQid(e) -> tt 0.001/0.001 isQid(i) -> tt 0.001/0.001 isQid(o) -> tt 0.001/0.001 isQid(u) -> tt 0.001/0.001 ) 0.001/0.001 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.001/0.001 0.001/0.001 0.001/0.001 Problem 1: 0.001/0.001 0.001/0.001 CleanTRS Processor: 0.001/0.001 0.001/0.001 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.001/0.001 Confluence Problem: 0.001/0.001 (VAR vNonEmpty:S I:S P:S V:S V1:S V2:S X:S Y:S Z:S) 0.001/0.001 (STRATEGY CONTEXTSENSITIVE 0.001/0.001 (__ 1 2) 0.001/0.001 (and 1) 0.001/0.001 (isList) 0.001/0.001 (isNeList) 0.001/0.001 (isNePal) 0.001/0.001 (isPal) 0.001/0.001 (isQid) 0.001/0.001 (a) 0.001/0.001 (e) 0.001/0.001 (fSNonEmpty) 0.001/0.001 (i) 0.001/0.001 (nil) 0.001/0.001 (o) 0.001/0.001 (tt) 0.001/0.001 (u) 0.001/0.001 ) 0.001/0.001 (RULES 0.001/0.001 __(__(X:S,Y:S),Z:S) -> __(X:S,__(Y:S,Z:S)) 0.001/0.001 __(nil,X:S) -> X:S 0.001/0.001 __(X:S,nil) -> X:S 0.001/0.001 and(tt,X:S) -> X:S 0.001/0.001 isList(__(V1:S,V2:S)) -> and(isList(V1:S),isList(V2:S)) 0.001/0.001 isList(nil) -> tt 0.001/0.001 isList(V:S) -> isNeList(V:S) 0.001/0.001 isNeList(__(V1:S,V2:S)) -> and(isList(V1:S),isNeList(V2:S)) 0.001/0.001 isNeList(__(V1:S,V2:S)) -> and(isNeList(V1:S),isList(V2:S)) 0.001/0.001 isNeList(V:S) -> isQid(V:S) 0.001/0.001 isNePal(__(I:S,__(P:S,I:S))) -> and(isQid(I:S),isPal(P:S)) 0.001/0.001 isNePal(V:S) -> isQid(V:S) 0.001/0.001 isPal(nil) -> tt 0.001/0.001 isPal(V:S) -> isNePal(V:S) 0.001/0.001 isQid(a) -> tt 0.001/0.001 isQid(e) -> tt 0.001/0.001 isQid(i) -> tt 0.001/0.001 isQid(o) -> tt 0.001/0.001 isQid(u) -> tt 0.001/0.001 ) 0.001/0.001 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.001/0.001 0.001/0.001 0.001/0.001 Problem 1: 0.001/0.001 0.001/0.001 Modular Confluence Combinations Decomposition Processor: 0.001/0.001 It is a CTRS -> No modular confluence 0.001/0.001 0.001/0.001 Problem 1: 0.001/0.001 Left-Homogeneous u-Replacing Variables Processor: 0.001/0.001 R satisfies LHRV condition 0.001/0.001 0.001/0.001 Problem 1: 0.001/0.001 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.001/0.001 Confluence Problem: 0.001/0.001 (VAR vNonEmpty:S I:S P:S V:S V1:S V2:S X:S Y:S Z:S) 0.001/0.001 (STRATEGY CONTEXTSENSITIVE 0.001/0.001 (__ 1 2) 0.001/0.001 (and 1) 0.001/0.001 (isList) 0.001/0.001 (isNeList) 0.001/0.001 (isNePal) 0.001/0.001 (isPal) 0.001/0.001 (isQid) 0.001/0.001 (a) 0.001/0.001 (e) 0.001/0.001 (fSNonEmpty) 0.001/0.001 (i) 0.001/0.001 (nil) 0.001/0.001 (o) 0.001/0.001 (tt) 0.001/0.001 (u) 0.001/0.001 ) 0.001/0.001 (RULES 0.001/0.001 __(__(X:S,Y:S),Z:S) -> __(X:S,__(Y:S,Z:S)) 0.001/0.001 __(nil,X:S) -> X:S 0.001/0.001 __(X:S,nil) -> X:S 0.001/0.001 and(tt,X:S) -> X:S 0.001/0.001 isList(__(V1:S,V2:S)) -> and(isList(V1:S),isList(V2:S)) 0.001/0.001 isList(nil) -> tt 0.001/0.001 isList(V:S) -> isNeList(V:S) 0.001/0.001 isNeList(__(V1:S,V2:S)) -> and(isList(V1:S),isNeList(V2:S)) 0.001/0.001 isNeList(__(V1:S,V2:S)) -> and(isNeList(V1:S),isList(V2:S)) 0.001/0.001 isNeList(V:S) -> isQid(V:S) 0.001/0.001 isNePal(__(I:S,__(P:S,I:S))) -> and(isQid(I:S),isPal(P:S)) 0.001/0.001 isNePal(V:S) -> isQid(V:S) 0.001/0.001 isPal(nil) -> tt 0.001/0.001 isPal(V:S) -> isNePal(V:S) 0.001/0.001 isQid(a) -> tt 0.001/0.001 isQid(e) -> tt 0.001/0.001 isQid(i) -> tt 0.001/0.001 isQid(o) -> tt 0.001/0.001 isQid(u) -> tt 0.001/0.001 ) 0.001/0.001 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.001/0.001 0.001/0.001 Huet Levy Processor: 0.001/0.001 -> Rules: 0.001/0.001 __(__(X:S,Y:S),Z:S) -> __(X:S,__(Y:S,Z:S)) 0.001/0.001 __(nil,X:S) -> X:S 0.001/0.001 __(X:S,nil) -> X:S 0.001/0.001 and(tt,X:S) -> X:S 0.001/0.001 isList(__(V1:S,V2:S)) -> and(isList(V1:S),isList(V2:S)) 0.001/0.001 isList(nil) -> tt 0.001/0.001 isList(V:S) -> isNeList(V:S) 0.001/0.001 isNeList(__(V1:S,V2:S)) -> and(isList(V1:S),isNeList(V2:S)) 0.001/0.001 isNeList(__(V1:S,V2:S)) -> and(isNeList(V1:S),isList(V2:S)) 0.001/0.001 isNeList(V:S) -> isQid(V:S) 0.001/0.001 isNePal(__(I:S,__(P:S,I:S))) -> and(isQid(I:S),isPal(P:S)) 0.001/0.001 isNePal(V:S) -> isQid(V:S) 0.001/0.001 isPal(nil) -> tt 0.001/0.001 isPal(V:S) -> isNePal(V:S) 0.001/0.001 isQid(a) -> tt 0.001/0.001 isQid(e) -> tt 0.001/0.001 isQid(i) -> tt 0.001/0.001 isQid(o) -> tt 0.001/0.001 isQid(u) -> tt 0.001/0.001 -> Vars: 0.001/0.001 X, Y, Z, X, X, X, V1, V2, V, V1, V2, V1, V2, V, I, P, V, V 0.001/0.001 -> UVars: 0.001/0.001 (UV-RuleId: 1, UV-LActive: [X, Y, Z], UV-RActive: [X, Y, Z], UV-LFrozen: [], UV-RFrozen: []) 0.001/0.001 (UV-RuleId: 2, UV-LActive: [X], UV-RActive: [X], UV-LFrozen: [], UV-RFrozen: []) 0.001/0.001 (UV-RuleId: 3, UV-LActive: [X], UV-RActive: [X], UV-LFrozen: [], UV-RFrozen: []) 0.001/0.001 (UV-RuleId: 4, UV-LActive: [], UV-RActive: [X], UV-LFrozen: [X], UV-RFrozen: []) 0.001/0.001 (UV-RuleId: 5, UV-LActive: [], UV-RActive: [], UV-LFrozen: [V1, V2], UV-RFrozen: [V1, V2]) 0.001/0.001 (UV-RuleId: 6, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.001/0.001 (UV-RuleId: 7, UV-LActive: [], UV-RActive: [], UV-LFrozen: [V], UV-RFrozen: [V]) 0.001/0.001 (UV-RuleId: 8, UV-LActive: [], UV-RActive: [], UV-LFrozen: [V1, V2], UV-RFrozen: [V1, V2]) 0.001/0.001 (UV-RuleId: 9, UV-LActive: [], UV-RActive: [], UV-LFrozen: [V1, V2], UV-RFrozen: [V1, V2]) 0.001/0.001 (UV-RuleId: 10, UV-LActive: [], UV-RActive: [], UV-LFrozen: [V], UV-RFrozen: [V]) 0.001/0.001 (UV-RuleId: 11, UV-LActive: [], UV-RActive: [], UV-LFrozen: [I, P], UV-RFrozen: [I, P]) 0.001/0.001 (UV-RuleId: 12, UV-LActive: [], UV-RActive: [], UV-LFrozen: [V], UV-RFrozen: [V]) 0.001/0.001 (UV-RuleId: 13, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.001/0.001 (UV-RuleId: 14, UV-LActive: [], UV-RActive: [], UV-LFrozen: [V], UV-RFrozen: [V]) 0.001/0.001 (UV-RuleId: 15, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.001/0.001 (UV-RuleId: 16, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.001/0.001 (UV-RuleId: 17, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.001/0.001 (UV-RuleId: 18, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.001/0.001 (UV-RuleId: 19, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.001/0.001 -> FVars: 0.001/0.001 x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23, x24, x25, x26 0.001/0.001 -> PVars: 0.001/0.001 X: [x9, x12, x13, x14], Y: [x10], Z: [x11], V1: [x15, x18, x20], V2: [x16, x19, x21], V: [x17, x22, x25, x26], I: [x23], P: [x24] 0.001/0.001 0.001/0.001 -> Rlps: 0.001/0.001 (rule: __(__(x9:S,x10:S),x11:S) -> __(x9:S,__(x10:S,x11:S)), id: 1, possubterms: __(__(x9:S,x10:S),x11:S)->[], __(x9:S,x10:S)->[1]) 0.001/0.001 (rule: __(nil,x12:S) -> x12:S, id: 2, possubterms: __(nil,x12:S)->[], nil->[1]) 0.001/0.001 (rule: __(x13:S,nil) -> x13:S, id: 3, possubterms: __(x13:S,nil)->[], nil->[2]) 0.001/0.001 (rule: and(tt,x14:S) -> x14:S, id: 4, possubterms: and(tt,x14:S)->[], tt->[1]) 0.001/0.001 (rule: isList(__(x15:S,x16:S)) -> and(isList(x15:S),isList(x16:S)), id: 5, possubterms: isList(__(x15:S,x16:S))->[]) 0.001/0.001 (rule: isList(nil) -> tt, id: 6, possubterms: isList(nil)->[]) 0.001/0.001 (rule: isList(x17:S) -> isNeList(x17:S), id: 7, possubterms: isList(x17:S)->[]) 0.001/0.001 (rule: isNeList(__(x18:S,x19:S)) -> and(isList(x18:S),isNeList(x19:S)), id: 8, possubterms: isNeList(__(x18:S,x19:S))->[]) 0.001/0.001 (rule: isNeList(__(x20:S,x21:S)) -> and(isNeList(x20:S),isList(x21:S)), id: 9, possubterms: isNeList(__(x20:S,x21:S))->[]) 0.001/0.001 (rule: isNeList(x22:S) -> isQid(x22:S), id: 10, possubterms: isNeList(x22:S)->[]) 0.001/0.001 (rule: isNePal(__(x23:S,__(x24:S,x23:S))) -> and(isQid(x23:S),isPal(x24:S)), id: 11, possubterms: isNePal(__(x23:S,__(x24:S,x23:S)))->[]) 0.001/0.001 (rule: isNePal(x25:S) -> isQid(x25:S), id: 12, possubterms: isNePal(x25:S)->[]) 0.001/0.001 (rule: isPal(nil) -> tt, id: 13, possubterms: isPal(nil)->[]) 0.001/0.001 (rule: isPal(x26:S) -> isNePal(x26:S), id: 14, possubterms: isPal(x26:S)->[]) 0.001/0.001 (rule: isQid(a) -> tt, id: 15, possubterms: isQid(a)->[]) 0.001/0.001 (rule: isQid(e) -> tt, id: 16, possubterms: isQid(e)->[]) 0.001/0.001 (rule: isQid(i) -> tt, id: 17, possubterms: isQid(i)->[]) 0.001/0.001 (rule: isQid(o) -> tt, id: 18, possubterms: isQid(o)->[]) 0.001/0.001 (rule: isQid(u) -> tt, id: 19, possubterms: isQid(u)->[]) 0.001/0.001 0.001/0.001 -> Unifications: 0.001/0.001 (R1 unifies with R1 at p: [1], l: __(__(x9:S,x10:S),x11:S), lp: __(x9:S,x10:S), sig: {x9:S -> __(X:S,Y:S),x10:S -> Z:S}, l': __(__(X:S,Y:S),Z:S), r: __(x9:S,__(x10:S,x11:S)), r': __(X:S,__(Y:S,Z:S))) 0.001/0.001 (R1 unifies with R2 at p: [1], l: __(__(x9:S,x10:S),x11:S), lp: __(x9:S,x10:S), sig: {x9:S -> nil,x10:S -> X:S}, l': __(nil,X:S), r: __(x9:S,__(x10:S,x11:S)), r': X:S) 0.001/0.001 (R1 unifies with R3 at p: [1], l: __(__(x9:S,x10:S),x11:S), lp: __(x9:S,x10:S), sig: {x9:S -> X:S,x10:S -> nil}, l': __(X:S,nil), r: __(x9:S,__(x10:S,x11:S)), r': X:S) 0.001/0.001 (R3 unifies with R1 at p: [], l: __(x13:S,nil), lp: __(x13:S,nil), sig: {Z:S -> nil,x13:S -> __(X:S,Y:S)}, l': __(__(X:S,Y:S),Z:S), r: x13:S, r': __(X:S,__(Y:S,Z:S))) 0.001/0.001 (R3 unifies with R2 at p: [], l: __(x13:S,nil), lp: __(x13:S,nil), sig: {X:S -> nil,x13:S -> nil}, l': __(nil,X:S), r: x13:S, r': X:S) 0.001/0.001 (R7 unifies with R5 at p: [], l: isList(x17:S), lp: isList(x17:S), sig: {x17:S -> __(V1:S,V2:S)}, l': isList(__(V1:S,V2:S)), r: isNeList(x17:S), r': and(isList(V1:S),isList(V2:S))) 0.001/0.001 (R7 unifies with R6 at p: [], l: isList(x17:S), lp: isList(x17:S), sig: {x17:S -> nil}, l': isList(nil), r: isNeList(x17:S), r': tt) 0.001/0.001 (R9 unifies with R8 at p: [], l: isNeList(__(x20:S,x21:S)), lp: isNeList(__(x20:S,x21:S)), sig: {x20:S -> V1:S,x21:S -> V2:S}, l': isNeList(__(V1:S,V2:S)), r: and(isNeList(x20:S),isList(x21:S)), r': and(isList(V1:S),isNeList(V2:S))) 0.001/0.001 (R10 unifies with R8 at p: [], l: isNeList(x22:S), lp: isNeList(x22:S), sig: {x22:S -> __(V1:S,V2:S)}, l': isNeList(__(V1:S,V2:S)), r: isQid(x22:S), r': and(isList(V1:S),isNeList(V2:S))) 0.001/0.001 (R10 unifies with R9 at p: [], l: isNeList(x22:S), lp: isNeList(x22:S), sig: {x22:S -> __(V1:S,V2:S)}, l': isNeList(__(V1:S,V2:S)), r: isQid(x22:S), r': and(isNeList(V1:S),isList(V2:S))) 0.001/0.001 (R12 unifies with R11 at p: [], l: isNePal(x25:S), lp: isNePal(x25:S), sig: {x25:S -> __(I:S,__(P:S,I:S))}, l': isNePal(__(I:S,__(P:S,I:S))), r: isQid(x25:S), r': and(isQid(I:S),isPal(P:S))) 0.001/0.001 (R14 unifies with R13 at p: [], l: isPal(x26:S), lp: isPal(x26:S), sig: {x26:S -> nil}, l': isPal(nil), r: isNePal(x26:S), r': tt) 0.001/0.001 0.001/0.001 -> Critical pairs info: 0.001/0.001 => Not trivial, Overlay, NW0, N1 0.001/0.001 => Trivial, Overlay, NW0, N2 0.001/0.001 <__(X:S,__(Y:S,nil)),__(X:S,Y:S)> => Not trivial, Overlay, NW0, N3 0.001/0.001 => Not trivial, Overlay, NW0, N4 0.001/0.001 => Not trivial, Overlay, NW0, N5 0.001/0.001 <__(X:S,Z:S),__(X:S,__(nil,Z:S))> => Not trivial, Not overlay, NW0, N6 0.001/0.001 => Not trivial, Overlay, NW0, N7 0.001/0.001 <__(X:S,Z:S),__(nil,__(X:S,Z:S))> => Not trivial, Not overlay, NW0, N8 0.001/0.001 => Not trivial, Overlay, NW0, N9 0.001/0.001 => Not trivial, Overlay, NW0, N10 0.001/0.001 <__(__(X:S,__(Y:S,Z:S)),Z:S),__(__(X:S,Y:S),__(Z:S,Z:S))> => Not trivial, Not overlay, NW0, N11 0.001/0.001 => Not trivial, Overlay, NW0, N12 0.001/0.001 0.001/0.001 -> Problem conclusions: 0.001/0.001 Not left linear, Right linear, Not linear 0.001/0.001 Not weakly orthogonal, Not almost orthogonal, Not orthogonal 0.001/0.001 Not Huet-Levy confluent, Not Newman confluent 0.001/0.001 R is a CS-TRS, Left-homogeneous u-replacing variables 0.001/0.001 0.001/0.001 0.001/0.001 Problem 1: 0.001/0.001 No Convergence Brute Force Processor: 0.001/0.001 -> Rewritings: 0.001/0.001 s: tt 0.001/0.001 Nodes: [0] 0.001/0.001 Edges: [] 0.001/0.001 ID: 0 => ('tt', D0) 0.001/0.001 t: isNeList(nil) 0.001/0.001 Nodes: [0,1] 0.001/0.001 Edges: [(0,1)] 0.001/0.001 ID: 0 => ('isNeList(nil)', D0) 0.001/0.001 ID: 1 => ('isQid(nil)', D1, R10, P[], S{x22:S -> nil}), NR: 'isQid(nil)' 0.001/0.001 tt ->* no union *<- isNeList(nil) 0.001/0.001 "Not joinable" 0.001/0.001 0.001/0.001 The problem is not joinable. 0.001/0.001 0.00user 0.00system 0:00.01elapsed 54%CPU (0avgtext+0avgdata 10404maxresident)k 0.001/0.001 0inputs+0outputs (0major+933minor)pagefaults 0swaps