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