NO Problem 1: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (VAR vNonEmpty) (REPLACEMENT-MAP (b) (c) (a) (f 1) (fSNonEmpty) (h 1, 2) ) (RULES b -> b c -> b c -> a c -> f(h(b,b)) ) ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Problem 1: CleanTRS Procedure: R was updated by simple cleaning of the TRS ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (VAR vNonEmpty) (REPLACEMENT-MAP (b) (c) (a) (f 1) (fSNonEmpty) (h 1, 2) ) (RULES c -> b c -> a c -> f(h(b,b)) ) ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Problem 1: Not CS-TRS Procedure: R is not a CS-TRS Problem 1: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (VAR vNonEmpty) (REPLACEMENT-MAP (b) (c) (a) (f 1) (fSNonEmpty) (h 1, 2) ) (RULES c -> b c -> a c -> f(h(b,b)) ) ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Huet Levy Procedure: -> Rules: c -> b c -> a c -> f(h(b,b)) -> Vars: -> Rlps: (rule: c -> b, id: 1, possubterms: c->[]) (rule: c -> a, id: 2, possubterms: c->[]) (rule: c -> f(h(b,b)), id: 3, possubterms: c->[]) -> Unifications: (R2 unifies with R1 at p: [], l: c, lp: c, sig: {}, l': c, r: a, r': b) (R3 unifies with R1 at p: [], l: c, lp: c, sig: {}, l': c, r: f(h(b,b)), r': b) (R3 unifies with R2 at p: [], l: c, lp: c, sig: {}, l': c, r: f(h(b,b)), r': a) -> Critical pairs info: => Not trivial, Overlay, Proper, NW0, N1 => Not trivial, Overlay, Proper, NW0, N2 => Not trivial, Overlay, Proper, NW0, N3 -> Problem conclusions: Left linear, Right linear, Linear Not weakly orthogonal, Not almost orthogonal, Not orthogonal Not Huet-Levy confluent, Not Newman confluent R is a TRS Problem 1: Different Normal CP Terms Procedure: => Not trivial, Overlay, Proper, NW0, N1, Normal and not trivial cp The problem is not confluent.