YES (VAR x y) (RULES k(a(),a()) -> a() h(x) -> a() f(g(x),y) -> a() ) (COMMENT Termination is shown by KBO with weight w0 = 1 w(f) = 0 w(g) = 1 w(a) = 1 w(h) = 1 w(k) = 0 and precedence: g > k > f > h > a )