YES We show the termination of the relative TRS R/S: R: f(x) -> x S: a() -> g(a()) -- SCC decomposition. Consider the non-minimal dependency pair problem (P, R), where P consists of (no rules) and R consists of: r1: f(x) -> x r2: a() -> g(a()) The estimated dependency graph contains the following SCCs: (no SCCs)