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