(VAR x)
(RULES 
  h(1(1(x))) -> 1(h(x))
  1(1(h(b(x)))) -> 1(1(s(b(x))))
  1(s(x)) -> s(1(x))
  b(s(x)) -> b(h(x))
  h(1(b(x))) -> t(1(1(b(x))))
  1(t(x)) -> t(1(1(1(x))))
  b(t(x)) -> b(h(x))
)
(COMMENT
TPDB SRS_Standard/Zantema_04/syracuse
)