(VAR ) (RULES b -> a f(h(b,f(a))) -> f(c) c -> h(c,c) h(f(f(b)),a) -> c h(a,a) -> a f(h(a,f(a))) -> f(c) h(f(f(a)),a) -> c )