YES We show the termination of the TRS R: p(f(f(x))) -> q(f(g(x))) p(g(g(x))) -> q(g(f(x))) q(f(f(x))) -> p(f(g(x))) q(g(g(x))) -> p(g(f(x))) -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: p#(f(f(x))) -> q#(f(g(x))) p2: p#(g(g(x))) -> q#(g(f(x))) p3: q#(f(f(x))) -> p#(f(g(x))) p4: q#(g(g(x))) -> p#(g(f(x))) and R consists of: r1: p(f(f(x))) -> q(f(g(x))) r2: p(g(g(x))) -> q(g(f(x))) r3: q(f(f(x))) -> p(f(g(x))) r4: q(g(g(x))) -> p(g(f(x))) The estimated dependency graph contains the following SCCs: (no SCCs)