YES
Time: 0.001335
TRS:
 {g1(x, x, y) -> h(x, y),
  g1(y, x, x) -> h(x, y),
      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),
  g2(x, y, y) -> h(x, y),
  g2(y, y, x) -> h(x, y),
      h(x, x) -> x}
 DP:
  DP:
   {g1#(x, x, y) -> h#(x, y),
    g1#(y, x, x) -> h#(x, y),
        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),
    g2#(x, y, y) -> h#(x, y),
    g2#(y, y, x) -> h#(x, y)}
  TRS:
  {g1(x, x, y) -> h(x, y),
   g1(y, x, x) -> h(x, y),
       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),
   g2(x, y, y) -> h(x, y),
   g2(y, y, x) -> h(x, y),
       h(x, x) -> x}
  EDG:
   {(f#(x, y) -> g2#(x, y, y), g2#(y, y, x) -> h#(x, y))
    (f#(x, y) -> g2#(x, y, y), g2#(x, y, y) -> h#(x, y))
    (f#(x, y) -> g2#(y, y, x), g2#(y, y, x) -> h#(x, y))
    (f#(x, y) -> g2#(y, y, x), g2#(x, y, y) -> h#(x, y))
    (f#(x, y) -> g1#(y, x, x), g1#(x, x, y) -> h#(x, y))
    (f#(x, y) -> g1#(y, x, x), g1#(y, x, x) -> h#(x, y))
    (f#(x, y) -> g1#(x, x, y), g1#(x, x, y) -> h#(x, y))
    (f#(x, y) -> g1#(x, x, y), g1#(y, x, x) -> h#(x, y))}
   SCCS (0):
    
    Qed