YES

(VAR x1 x0 x2 y x z)
(RULES
  symm(trans(x1,x0)) -> trans(symm(x0),symm(x1))
  symm(h(x0)) -> h(symm(x0))
  symm(g(x0)) -> g(symm(x0))
  symm(f(x0)) -> f(symm(x0))
  trans(trans(x0,x1),symm(x1)) -> x0
  symm(symm(x0)) -> x0
  symm(refl()) -> refl()
  f(refl()) -> refl()
  g(refl()) -> refl()
  h(refl()) -> refl()
  trans(x0,symm(x0)) -> refl()
  trans(x0,refl()) -> x0
  trans(trans(x0,f(x1)),g(x2)) -> trans(trans(x0,g(x2)),f(x1))
  trans(trans(x0,g(x2)),h(x1)) -> trans(trans(x0,h(x1)),g(x2))
  trans(trans(x0,f(x1)),h(x2)) -> trans(trans(x0,h(x2)),f(x1))
  trans(trans(x0,f(x1)),f(x2)) -> trans(x0,f(trans(x1,x2)))
  trans(trans(x0,g(x1)),g(x2)) -> trans(x0,g(trans(x1,x2)))
  trans(trans(x0,h(x1)),h(x2)) -> trans(x0,h(trans(x1,x2)))
  trans(trans(x0,symm(x1)),x1) -> x0
  trans(f(y),h(x)) -> trans(h(x),f(y))
  trans(g(x),h(y)) -> trans(h(y),g(x))
  trans(f(x),g(y)) -> trans(g(y),f(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(refl(),x) -> x
  trans(symm(x),x) -> refl()
  trans(x,trans(y,z)) -> trans(trans(x,y),z)
)

(COMMENT
Termination is shown by EKBO with interpretations on natural numbers

  trans_A(x1,x2) = x1 + x2 + 1
  symm_A(x1) = x1
  refl_A = 1
  f_A(x1) = 1
  g_A(x1) = 2
  h_A(x1) = x1 + 3
  trans#_A(x1,x2) = x2
  refl#_A = 0
  g#_A(x1) = x1

weights

  w0 = 1
  w(trans) = 0
  w(symm) = 0
  w(refl) = 1
  w(f) = 1
  w(g) = 1
  w(h) = 1

and precedence:

symm > f > h > trans > g > refl
)