YES (VAR x z y x0 x1) (RULES f8(f8(f8(f8(x)))) -> f8(x) f8(j(z)) -> f8(f8(z)) f2(y) -> f8(y) f3(y) -> f8(y) f4(y) -> f8(y) f5(y) -> f8(y) f6(y) -> f8(y) f7(y) -> f8(y) f1(y) -> f8(y) f9(y) -> f8(y) f10(y) -> f8(y) f11(y) -> f8(y) f12(y) -> f8(y) f13(y) -> f8(y) f14(y) -> f8(y) g(x0,x1) -> f8(x1) ) (COMMENT Termination is shown by ELPO with interpretations on natural numbers g_A(x1,x2) = x2 + 1 j_A(x1) = x1 + 2 f1_A(x1) = x1 + 1 f2_A(x1) = x1 + 1 f3_A(x1) = x1 + 1 f4_A(x1) = x1 + 1 f5_A(x1) = x1 + 1 f6_A(x1) = x1 + 1 f7_A(x1) = x1 + 1 f8_A(x1) = x1 + 1 f9_A(x1) = x1 + 1 f10_A(x1) = x1 + 1 f11_A(x1) = x1 + 1 f12_A(x1) = x1 + 1 f13_A(x1) = x1 + 1 f14_A(x1) = x1 + 1 g#_A(x1,x2) = 0 j#_A(x1) = x1 f13#_A(x1) = x1 f14#_A(x1) = 0 and precedence: g > j > f14 > f13 > f10 > f6 > f9 > f3 > f11 > f4 > f2 > f5 > f12 > f1 > f7 > f8 )