YES
(VAR x y z)
(RULES
trans(g(x),h(y)) -> trans(h(y),g(x))
trans(h(x),h(y)) -> h(trans(x,y))
trans(g(x),g(y)) -> g(trans(x,y))
trans(f(x),f(y)) -> f(trans(x,y))
trans(symm(x),x) -> refl()
trans(g(x),trans(h(y),z)) -> trans(h(y),trans(g(x),z))
trans(f(x),trans(f(y),z)) -> trans(f(trans(x,y)),z)
trans(g(x),trans(g(y),z)) -> trans(g(trans(x,y)),z)
trans(h(x),trans(h(y),z)) -> trans(h(trans(x,y)),z)
trans(x,symm(x)) -> refl()
symm(h(x)) -> h(symm(x))
symm(g(x)) -> g(symm(x))
symm(f(x)) -> f(symm(x))
symm(trans(x,y)) -> trans(symm(y),symm(x))
trans(x,trans(symm(x),y)) -> y
symm(refl()) -> refl()
symm(symm(x)) -> x
h(refl()) -> refl()
f(refl()) -> refl()
g(refl()) -> refl()
trans(x,refl()) -> x
trans(symm(x),trans(x,y)) -> y
trans(g(x),trans(f(y),z)) -> trans(f(y),trans(g(x),z))
trans(h(x),trans(f(y),z)) -> trans(f(y),trans(h(x),z))
trans(trans(x,y),z) -> trans(x,trans(y,z))
trans(refl(),x) -> x
trans(g(x),f(y)) -> trans(f(y),g(x))
trans(h(x),f(y)) -> trans(f(y),h(x))
)