(VAR x)
(RULES
  a(x) -> b(x)
  b(b(c(x))) -> c(a(c(a(a(x)))))
  c(c(x)) -> x
)
(COMMENT
TPDB SRS_Standard/Waldmann_07_size12/size-12-alpha-3-num-412
)