YES

Problem:
 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()

Proof:
 DP Processor:
  DPs:
   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#(y)
   s#(g(x,y)) -> s#(x)
   s#(g(x,y)) -> g#(s(x),s(y))
   f#(g(x,y),g(u,v)) -> f#(y,v)
   f#(g(x,y),g(u,v)) -> f#(x,u)
   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()
  ADG Processor:
   DPs:
    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#(y)
    s#(g(x,y)) -> s#(x)
    s#(g(x,y)) -> g#(s(x),s(y))
    f#(g(x,y),g(u,v)) -> f#(y,v)
    f#(g(x,y),g(u,v)) -> f#(x,u)
    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()
   graph:
    f#(g(x,y),g(u,v)) -> f#(y,v) -> f#(g(x,y),g(u,v)) -> f#(y,v)
    f#(g(x,y),g(u,v)) -> f#(y,v) -> 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))
    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)) -> f#(x,u) -> f#(g(x,y),g(u,v)) -> f#(x,u)
    f#(g(x,y),g(u,v)) -> f#(x,u) -> f#(g(x,y),g(u,v)) -> g#(f(x,u),f(y,v))
    s#(g(x,y)) -> s#(y) -> s#(f(x,y)) -> s#(x)
    s#(g(x,y)) -> s#(y) -> s#(f(x,y)) -> s#(y)
    s#(g(x,y)) -> s#(y) -> s#(f(x,y)) -> f#(s(y),s(x))
    s#(g(x,y)) -> s#(y) -> s#(g(x,y)) -> s#(y)
    s#(g(x,y)) -> s#(y) -> s#(g(x,y)) -> s#(x)
    s#(g(x,y)) -> s#(y) -> s#(g(x,y)) -> g#(s(x),s(y))
    s#(g(x,y)) -> s#(x) -> s#(f(x,y)) -> s#(x)
    s#(g(x,y)) -> s#(x) -> s#(f(x,y)) -> s#(y)
    s#(g(x,y)) -> s#(x) -> 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)) -> s#(x) -> s#(g(x,y)) -> s#(x)
    s#(g(x,y)) -> s#(x) -> s#(g(x,y)) -> g#(s(x),s(y))
    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)
    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)) -> s#(y) -> s#(f(x,y)) -> s#(x)
    s#(f(x,y)) -> s#(y) -> s#(f(x,y)) -> s#(y)
    s#(f(x,y)) -> s#(y) -> s#(f(x,y)) -> f#(s(y),s(x))
    s#(f(x,y)) -> s#(y) -> s#(g(x,y)) -> s#(y)
    s#(f(x,y)) -> s#(y) -> s#(g(x,y)) -> s#(x)
    s#(f(x,y)) -> s#(y) -> s#(g(x,y)) -> g#(s(x),s(y))
    s#(f(x,y)) -> s#(x) -> s#(f(x,y)) -> s#(x)
    s#(f(x,y)) -> s#(x) -> s#(f(x,y)) -> s#(y)
    s#(f(x,y)) -> s#(x) -> s#(f(x,y)) -> f#(s(y),s(x))
    s#(f(x,y)) -> s#(x) -> s#(g(x,y)) -> s#(y)
    s#(f(x,y)) -> s#(x) -> s#(g(x,y)) -> s#(x)
    s#(f(x,y)) -> s#(x) -> s#(g(x,y)) -> g#(s(x),s(y))
   Restore Modifier:
    DPs:
     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#(y)
     s#(g(x,y)) -> s#(x)
     s#(g(x,y)) -> g#(s(x),s(y))
     f#(g(x,y),g(u,v)) -> f#(y,v)
     f#(g(x,y),g(u,v)) -> f#(x,u)
     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()
    SCC Processor:
     #sccs: 2
     #rules: 6
     #arcs: 33/81
     DPs:
      s#(g(x,y)) -> s#(y)
      s#(g(x,y)) -> s#(x)
      s#(f(x,y)) -> s#(y)
      s#(f(x,y)) -> s#(x)
     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()
     Matrix Interpretation Processor:
      dimension: 1
      interpretation:
       [s#](x0) = x0 + 1,
       
       [g](x0, x1) = x0 + x1 + 1,
       
       [f](x0, x1) = x0 + x1 + 1,
       
       [s](x0) = x0,
       
       [a] = 0
      orientation:
       s#(g(x,y)) = x + y + 2 >= y + 1 = s#(y)
       
       s#(g(x,y)) = x + y + 2 >= x + 1 = s#(x)
       
       s#(f(x,y)) = x + y + 2 >= y + 1 = s#(y)
       
       s#(f(x,y)) = x + y + 2 >= x + 1 = s#(x)
       
       s(a()) = 0 >= 0 = a()
       
       s(s(x)) = x >= x = x
       
       s(f(x,y)) = x + y + 1 >= x + y + 1 = f(s(y),s(x))
       
       s(g(x,y)) = x + y + 1 >= x + y + 1 = g(s(x),s(y))
       
       f(x,a()) = x + 1 >= x = x
       
       f(a(),y) = y + 1 >= y = y
       
       f(g(x,y),g(u,v)) = u + v + x + y + 3 >= u + v + x + y + 3 = g(f(x,u),f(y,v))
       
       g(a(),a()) = 1 >= 0 = a()
      problem:
       DPs:
        
       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()
      Qed
     
     DPs:
      f#(g(x,y),g(u,v)) -> f#(y,v)
      f#(g(x,y),g(u,v)) -> f#(x,u)
     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()
     Matrix Interpretation Processor:
      dimension: 1
      interpretation:
       [f#](x0, x1) = x1 + 1,
       
       [g](x0, x1) = x0 + x1 + 1,
       
       [f](x0, x1) = x0 + x1,
       
       [s](x0) = x0,
       
       [a] = 0
      orientation:
       f#(g(x,y),g(u,v)) = u + v + 2 >= v + 1 = f#(y,v)
       
       f#(g(x,y),g(u,v)) = u + v + 2 >= u + 1 = f#(x,u)
       
       s(a()) = 0 >= 0 = a()
       
       s(s(x)) = x >= x = x
       
       s(f(x,y)) = x + y >= x + y = f(s(y),s(x))
       
       s(g(x,y)) = x + y + 1 >= x + y + 1 = g(s(x),s(y))
       
       f(x,a()) = x >= x = x
       
       f(a(),y) = y >= y = y
       
       f(g(x,y),g(u,v)) = u + v + x + y + 2 >= u + v + x + y + 1 = g(f(x,u),f(y,v))
       
       g(a(),a()) = 1 >= 0 = a()
      problem:
       DPs:
        
       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()
      Qed