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