YES
Time: 0.017102
TRS:
 {        a(x, g()) -> a(f(), a(g(), a(f(), x))),
  a(f(), a(f(), x)) -> a(x, g())}
 DP:
  DP:
   {        a#(x, g()) -> a#(g(), a(f(), x)),
            a#(x, g()) -> a#(f(), x),
            a#(x, g()) -> a#(f(), a(g(), a(f(), x))),
    a#(f(), a(f(), x)) -> a#(x, g())}
  TRS:
  {        a(x, g()) -> a(f(), a(g(), a(f(), x))),
   a(f(), a(f(), x)) -> a(x, g())}
  UR:
   {        a(x, g()) -> a(f(), a(g(), a(f(), x))),
    a(f(), a(f(), x)) -> a(x, g())}
   EDG:
    {(a#(f(), a(f(), x)) -> a#(x, g()), a#(x, g()) -> a#(f(), a(g(), a(f(), x))))
     (a#(f(), a(f(), x)) -> a#(x, g()), a#(x, g()) -> a#(f(), x))
     (a#(f(), a(f(), x)) -> a#(x, g()), a#(x, g()) -> a#(g(), a(f(), x)))
     (a#(x, g()) -> a#(f(), x), a#(x, g()) -> a#(g(), a(f(), x)))
     (a#(x, g()) -> a#(f(), x), a#(x, g()) -> a#(f(), x))
     (a#(x, g()) -> a#(f(), x), a#(x, g()) -> a#(f(), a(g(), a(f(), x))))
     (a#(x, g()) -> a#(f(), x), a#(f(), a(f(), x)) -> a#(x, g()))}
    STATUS:
     arrows: 0.562500
     SCCS (1):
      Scc:
       {        a#(x, g()) -> a#(f(), x),
        a#(f(), a(f(), x)) -> a#(x, g())}
      
      SCC (2):
       Strict:
        {        a#(x, g()) -> a#(f(), x),
         a#(f(), a(f(), x)) -> a#(x, g())}
       Weak:
       {        a(x, g()) -> a(f(), a(g(), a(f(), x))),
        a(f(), a(f(), x)) -> a(x, g())}
       POLY:
        Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
        Interpretation:
         [a](x0, x1) = x0 + x1,
         
         [g] = 1,
         
         [f] = 1,
         
         [a#](x0, x1) = x0 + x1 + 1
        Strict:
         a#(f(), a(f(), x)) -> a#(x, g())
         3 + 1x >= 2 + 1x
         a#(x, g()) -> a#(f(), x)
         2 + 1x >= 2 + 1x
        Weak:
         a(f(), a(f(), x)) -> a(x, g())
         2 + 1x >= 1 + 1x
         a(x, g()) -> a(f(), a(g(), a(f(), x)))
         1 + 1x >= 3 + 1x
       SCCS (1):
        Scc:
         {a#(x, g()) -> a#(f(), x)}
        
        SCC (1):
         Strict:
          {a#(x, g()) -> a#(f(), x)}
         Weak:
         {        a(x, g()) -> a(f(), a(g(), a(f(), x))),
          a(f(), a(f(), x)) -> a(x, g())}
         POLY:
          Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
          Interpretation:
           [a](x0, x1) = 0,
           
           [g] = 1,
           
           [f] = 0,
           
           [a#](x0, x1) = x0 + x1 + 1
          Strict:
           a#(x, g()) -> a#(f(), x)
           2 + 1x >= 1 + 1x
          Weak:
           a(f(), a(f(), x)) -> a(x, g())
           0 + 0x >= 0 + 0x
           a(x, g()) -> a(f(), a(g(), a(f(), x)))
           0 + 0x >= 0 + 0x
         Qed