YES Problem 1: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (VAR vNonEmpty) (REPLACEMENT-MAP (a) (c) (f 1) (fSNonEmpty) ) (RULES a -> f(c) c -> c ) ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Problem 1: CleanTRS Procedure: R was updated by simple cleaning of the TRS ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (VAR vNonEmpty) (REPLACEMENT-MAP (a) (c) (f 1) (fSNonEmpty) ) (RULES a -> f(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) (c) (f 1) (fSNonEmpty) ) (RULES a -> f(c) ) Linear:YES ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Huet Levy Procedure: -> Rules: a -> f(c) -> Vars: -> Rlps: (rule: a -> f(c), id: 1, possubterms: a->[]) -> 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.