YES

We show the termination of the TRS R:

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

-- SCC decomposition.

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

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

and R consists of:

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

The estimated dependency graph contains the following SCCs:

  (no SCCs)