YES

We show the termination of the TRS R:

  f(x,y) -> g1(x,x,y)
  f(x,y) -> g1(y,x,x)
  f(x,y) -> g2(x,y,y)
  f(x,y) -> g2(y,y,x)
  g1(x,x,y) -> h(x,y)
  g1(y,x,x) -> h(x,y)
  g2(x,y,y) -> h(x,y)
  g2(y,y,x) -> h(x,y)
  h(x,x) -> x

-- SCC decomposition.

Consider the dependency pair problem (P, R), where P consists of

p1: f#(x,y) -> g1#(x,x,y)
p2: f#(x,y) -> g1#(y,x,x)
p3: f#(x,y) -> g2#(x,y,y)
p4: f#(x,y) -> g2#(y,y,x)
p5: g1#(x,x,y) -> h#(x,y)
p6: g1#(y,x,x) -> h#(x,y)
p7: g2#(x,y,y) -> h#(x,y)
p8: g2#(y,y,x) -> h#(x,y)

and R consists of:

r1: f(x,y) -> g1(x,x,y)
r2: f(x,y) -> g1(y,x,x)
r3: f(x,y) -> g2(x,y,y)
r4: f(x,y) -> g2(y,y,x)
r5: g1(x,x,y) -> h(x,y)
r6: g1(y,x,x) -> h(x,y)
r7: g2(x,y,y) -> h(x,y)
r8: g2(y,y,x) -> h(x,y)
r9: h(x,x) -> x

The estimated dependency graph contains the following SCCs:

  (no SCCs)