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