(VAR x y) 
(RULES
  g(f(b,x)) -> g(h(h(f(f(h(k(k(x,x),x)),h(k(k(x,x),x))),h(k(k(x,x),x))))))
  f(x,b) -> h(f(f(x,x),x))
  k(x,y) -> q(x,y,y)
  q(x,y,b) -> r(x,y)
  r(x,b) -> f(x,b)
)
(COMMENT
from van Oostrom (AJSW 2016)
submitted by: Vincent van Oostrom
)