(VAR x y z)
(RULES
  *(x,*(y,z)) -> *(*(x,y),z)
  *(*(x,y),z) -> *(x,*(y,z))

  eq(*(a,x),*(y,a)) -> eq(x,y)
  eq(a,a)           -> T
  eq(a,*(x,y))      -> F
  eq(x,y)           -> eq(y,x)
)
(COMMENT
  the TRS R2 in Section 3
)