(VAR x)
(RULES
  g0(g0(g0(x))) -> c0
  g0(g0(c0)) -> c0
  g0(c0) -> c0
  g0(g0(g1(g1(x)))) -> g0(c0)
  g1(g0(c0)) -> c0
  g1(c0) -> c0
)
(COMMENT from p.29 of \cite{IWC16})