YES (VAR x z y x0 x1) (RULES f2(f2(f2(f2(x)))) -> f2(x) f2(j(z)) -> f2(f2(z)) f3(y) -> f2(y) f8(y) -> f2(y) f4(y) -> f2(y) f5(y) -> f2(y) f6(y) -> f2(y) f7(y) -> f2(y) f1(y) -> f2(y) g(x0,x1) -> f2(x1) ) (COMMENT Termination is shown by LPO with precedence: g > f6 > f5 > f4 > f7 > f1 > f8 > f3 > j > f2 )