YES 1 decompositions #1 ----------- 2: a() -> b() 4: b() -> a() 5: b() -> c() @Rule Labeling --- R 2: a() -> b() 4: b() -> a() 5: b() -> c() --- S 2: a() -> b() 4: b() -> a() 5: b() -> c() NOTE: input TRS is reduced original is 1: f(a(),a(),b(),b()) -> f(c(),c(),c(),c()) 2: a() -> b() 3: a() -> c() 4: b() -> a() 5: b() -> c() reduced to 2: a() -> b() 4: b() -> a() 5: b() -> c()