(VAR x)
(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,b) -> q(x)
  q(x) -> f(x,b)
)
(COMMENT should be hot-confluent, cf. VvO presentation at AJSW 2016)