YES Problem 1: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (VAR vNonEmpty) (REPLACEMENT-MAP (b) (c) (a) (fSNonEmpty) ) (RULES b -> a c -> b ) ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Problem 1: 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 (b) (c) (a) (fSNonEmpty) ) (RULES b -> a c -> b ) Linear:YES ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Huet Levy Procedure: -> Rules: b -> a c -> b -> Vars: -> Rlps: (rule: b -> a, id: 1, possubterms: b->[]) (rule: c -> b, id: 2, possubterms: c->[]) -> 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.