(VAR x)
(RULES
  b(a(a(b(b(x))))) -> b(a(a(a(a(b(b(x)))))))
  b(a(b(b(x)))) -> b(b(x))
  b(a(b(a(a(a(a(b(x)))))))) -> b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x))))))))))))))))))))))
  b(a(a(b(a(a(a(a(b(x))))))))) -> b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(x)))))))))))))))
  b(a(a(a(b(a(a(a(a(b(x)))))))))) -> b(x)
)
(COMMENT
TPDB SRS_Standard/Trafo_06/un02
)