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) = x2 + 28958 h_A(x1) = 1 j_A(x1) = 0 g_A(x1) = x1 i_A(x1) = x1 + 28959 f#_A(x1,x2) = x1 + x2 h#_A(x1) = x1 j#_A(x1) = x1 g#_A(x1) = x1 i#_A(x1) = x1 and precedence: h > i > f > j > g )