(VAR x)
(RULES
  f(f(x,a),a) -> f(f(f(f(a,f(a,x)),a),a),a)
)
(COMMENT
submitted by: Johannes Waldmann
)