YES Problem 1: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (VAR vNonEmpty) (REPLACEMENT-MAP (a) (b) (c) (fSNonEmpty) ) (RULES a -> a b -> c ) ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Problem 1: CleanTRS Procedure: R was updated by simple cleaning of the TRS ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (VAR vNonEmpty) (REPLACEMENT-MAP (a) (b) (c) (fSNonEmpty) ) (RULES b -> c ) ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Problem 1: Not CS-TRS Procedure: R is not a CS-TRS Problem 1: Linearity Procedure: Linear? YES Problem 1: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (VAR vNonEmpty) (REPLACEMENT-MAP (a) (b) (c) (fSNonEmpty) ) (RULES b -> c ) Linear:YES ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Huet Levy Procedure: -> Rules: b -> c -> Vars: -> Rlps: (rule: b -> c, id: 1, possubterms: b->[]) -> Unifications: -> Critical pairs info: -> Problem conclusions: Left linear, Right linear, Linear Weakly orthogonal, Almost orthogonal, Orthogonal Huet-Levy confluent, Not Newman confluent R is a TRS The problem is confluent.