YES 1: g(a()) -> f(g(a())) 2: g(b()) -> c() 3: a() -> b() 4: f(x1) -> h(x1,x1) 5: h(x1,x2) -> c() @Rule Labeling --- R 1: g(a()) -> f(g(a())) 2: g(b()) -> c() 3: a() -> b() 4: f(x1) -> h(x1,x1) 5: h(x1,x2) -> c() --- S 1: g(a()) -> f(g(a())) 2: g(b()) -> c() 3: a() -> b() 4: f(x1) -> h(x1,x1) 5: h(x1,x2) -> c()