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