(VAR x ) (RULES b -> a b -> c c -> c d -> c d -> e f(x,a) -> A f(x,e) -> A f(x,A) -> A f(c,x) -> A c -> a e -> c f(a,x) -> A f(x,c) -> A )