YES
Time: 0.008537
TRS:
 {              s a() -> a(),
                s s x -> x,
            s f(x, y) -> f(s y, s x),
            s g(x, y) -> g(s x, s y),
            f(x, a()) -> x,
            f(a(), y) -> y,
  f(g(x, y), g(u, v)) -> g(f(x, u), f(y, v)),
          g(a(), a()) -> a()}
 DP:
  DP:
   {          s# f(x, y) -> s# x,
              s# f(x, y) -> s# y,
              s# f(x, y) -> f#(s y, s x),
              s# g(x, y) -> s# x,
              s# g(x, y) -> s# y,
              s# g(x, y) -> g#(s x, s y),
    f#(g(x, y), g(u, v)) -> f#(x, u),
    f#(g(x, y), g(u, v)) -> f#(y, v),
    f#(g(x, y), g(u, v)) -> g#(f(x, u), f(y, v))}
  TRS:
  {              s a() -> a(),
                 s s x -> x,
             s f(x, y) -> f(s y, s x),
             s g(x, y) -> g(s x, s y),
             f(x, a()) -> x,
             f(a(), y) -> y,
   f(g(x, y), g(u, v)) -> g(f(x, u), f(y, v)),
           g(a(), a()) -> a()}
  UR:
   {              s a() -> a(),
                  s s x -> x,
              s f(x, y) -> f(s y, s x),
              s g(x, y) -> g(s x, s y),
              f(x, a()) -> x,
              f(a(), y) -> y,
    f(g(x, y), g(u, v)) -> g(f(x, u), f(y, v)),
            g(a(), a()) -> a()}
   EDG:
    {(s# f(x, y) -> f#(s y, s x), f#(g(x, y), g(u, v)) -> g#(f(x, u), f(y, v)))
     (s# f(x, y) -> f#(s y, s x), f#(g(x, y), g(u, v)) -> f#(y, v))
     (s# f(x, y) -> f#(s y, s x), f#(g(x, y), g(u, v)) -> f#(x, u))}
    STATUS:
     arrows: 0.962963
     SCCS (0):