(VAR x y)
(RULES 
 f(x) -> g(x)
 a(x,y) -> a(f(x),f(x))
 b(x,y) -> c(x,x)
 c(x,x) -> c(f(x),f(x))
)
(COMMENT from the collection of \cite{SAT2013})