YES NOTE: input TRS is reduced original is 6: c2() -> g0(f0(c1(),c1())) 7: c2() -> c1() 8: c1() -> c1() 9: c2() -> c0() reduced to 6: c2() -> g0(f0(c1(),c1())) 7: c2() -> c1() 9: c2() -> c0() NOTE: input TRS is reduced original is 1: c0() -> c0() 2: c0() -> c1() 3: c0() -> f0(c0(),c0()) 4: f0(c1(),c1()) -> f0(c0(),c0()) 5: f0(x1,c0()) -> f0(c0(),c1()) reduced to 2: c0() -> c1() 3: c0() -> f0(c0(),c0()) 4: f0(c1(),c1()) -> f0(c0(),c0()) 5: f0(x1,c0()) -> f0(c0(),c1()) 0.83