YES (VAR x0 x y) (RULES g(j(h(x0))) -> i(h(x0)) g(f(x,x)) -> i(x) f(h(x),y) -> j(h(x)) f(x,h(y)) -> j(x) ) (COMMENT Termination is shown by EKBO with interpretations on natural numbers f_A(x1,x2) = x1 + x2 + 1 h_A(x1) = x1 + 29243 j_A(x1) = x1 + 1 g_A(x1) = x1 i_A(x1) = 0 f#_A(x1,x2) = x1 + x2 weights w0 = 2 w(f) = 0 w(h) = 1 w(j) = 1 w(g) = 1 w(i) = 1 and precedence: h > f > j > g > i )