YES 1: f(g(x1,a(),b())) -> x1 2: g(f(h(c(),d())),x1,x2) -> h(k1(x1),k2(x2)) 3: k1(a()) -> c() 4: k2(b()) -> d() @Jouannaud and Kirchner's criterion --- R 1: f(g(x1,a(),b())) -> x1 2: g(f(h(c(),d())),x1,x2) -> h(k1(x1),k2(x2)) 3: k1(a()) -> c() 4: k2(b()) -> d() --- S 1: f(g(x1,a(),b())) -> x1 2: g(f(h(c(),d())),x1,x2) -> h(k1(x1),k2(x2)) 3: k1(a()) -> c() 4: k2(b()) -> d() NOTE: input TRS is reduced original is 1: f(g(x1,a(),b())) -> x1 2: g(f(h(c(),d())),x1,x2) -> h(k1(x1),k2(x2)) 3: k1(a()) -> c() 4: k2(b()) -> d() 5: f(h(k1(a()),k2(b()))) -> f(h(c(),d())) 6: f(h(c(),k2(b()))) -> f(h(c(),d())) 7: f(h(k1(a()),d())) -> f(h(c(),d())) reduced to 1: f(g(x1,a(),b())) -> x1 2: g(f(h(c(),d())),x1,x2) -> h(k1(x1),k2(x2)) 3: k1(a()) -> c() 4: k2(b()) -> d()