YES

Problem:
 a(f(),a(f(),a(g(),a(g(),x)))) -> a(g(),a(g(),a(g(),a(f(),a(f(),a(f(),x))))))

Proof:
 Uncurry Processor:
  f1(f1(g1(g1(x)))) -> g1(g1(g1(f1(f1(f1(x))))))
  a(f(),x1) -> f1(x1)
  a(g(),x1) -> g1(x1)
  Matrix Interpretation Processor: dim=3
   
   interpretation:
               [1 0 0]  
    [g1](x0) = [0 1 0]x0
               [0 1 0]  ,
    
               [1 0 0]     [0]
    [f1](x0) = [0 0 0]x0 + [0]
               [0 0 0]     [1],
    
                  [1 0 0]     [1 1 1]     [0]
    [a](x0, x1) = [1 0 0]x0 + [1 1 1]x1 + [0]
                  [0 0 0]     [1 1 1]     [1],
    
          [0]
    [g] = [0]
          [0],
    
          [1]
    [f] = [0]
          [0]
   orientation:
                        [1 0 0]    [0]    [1 0 0]                             
    f1(f1(g1(g1(x)))) = [0 0 0]x + [0] >= [0 0 0]x = g1(g1(g1(f1(f1(f1(x))))))
                        [0 0 0]    [1]    [0 0 0]                             
    
                [1 1 1]     [1]    [1 0 0]     [0]         
    a(f(),x1) = [1 1 1]x1 + [1] >= [0 0 0]x1 + [0] = f1(x1)
                [1 1 1]     [1]    [0 0 0]     [1]         
    
                [1 1 1]     [0]    [1 0 0]           
    a(g(),x1) = [1 1 1]x1 + [0] >= [0 1 0]x1 = g1(x1)
                [1 1 1]     [1]    [0 1 0]           
   problem:
    f1(f1(g1(g1(x)))) -> g1(g1(g1(f1(f1(f1(x))))))
    a(g(),x1) -> g1(x1)
   Matrix Interpretation Processor: dim=3
    
    interpretation:
                [1 0 0]  
     [g1](x0) = [0 0 0]x0
                [0 0 0]  ,
     
                [1 0 0]  
     [f1](x0) = [0 0 0]x0
                [0 0 0]  ,
     
                   [1 0 0]     [1 0 0]     [1]
     [a](x0, x1) = [0 0 0]x0 + [0 0 0]x1 + [1]
                   [0 1 0]     [0 1 0]     [0],
     
           [0]
     [g] = [1]
           [0]
    orientation:
                         [1 0 0]     [1 0 0]                             
     f1(f1(g1(g1(x)))) = [0 0 0]x >= [0 0 0]x = g1(g1(g1(f1(f1(f1(x))))))
                         [0 0 0]     [0 0 0]                             
     
                 [1 0 0]     [1]    [1 0 0]           
     a(g(),x1) = [0 0 0]x1 + [1] >= [0 0 0]x1 = g1(x1)
                 [0 1 0]     [1]    [0 0 0]           
    problem:
     f1(f1(g1(g1(x)))) -> g1(g1(g1(f1(f1(f1(x))))))
    Bounds Processor:
     bound: 3
     enrichment: match
     automaton:
      final states: {1}
      transitions:
       f{1,2}(57) -> 58*
       f{1,2}(37) -> 38*
       f{1,2}(59) -> 60*
       f{1,2}(36) -> 37*
       f{1,2}(58) -> 59*
       f{1,2}(38) -> 39*
       f50() -> 2*
       g{1,3}(67) -> 68*
       g{1,3}(69) -> 70*
       g{1,3}(68) -> 69*
       g{1,0}(5) -> 6*
       g{1,0}(7) -> 1*
       g{1,0}(6) -> 7*
       f{1,3}(65) -> 66*
       f{1,3}(64) -> 65*
       f{1,3}(66) -> 67*
       f{1,0}(2) -> 3*
       f{1,0}(4) -> 5*
       f{1,0}(3) -> 4*
       g{1,1}(32) -> 33*
       g{1,1}(12) -> 13*
       g{1,1}(34) -> 35*
       g{1,1}(11) -> 12*
       g{1,1}(33) -> 34*
       g{1,1}(13) -> 14*
       f{1,1}(30) -> 31*
       f{1,1}(10) -> 11*
       f{1,1}(29) -> 30*
       f{1,1}(9) -> 10*
       f{1,1}(31) -> 32*
       f{1,1}(8) -> 9*
       g{1,2}(60) -> 61*
       g{1,2}(40) -> 41*
       g{1,2}(62) -> 63*
       g{1,2}(39) -> 40*
       g{1,2}(61) -> 62*
       g{1,2}(41) -> 42*
       1 -> 3,4
       6 -> 8*
       11 -> 36*
       13 -> 29*
       14 -> 5*
       33 -> 57*
       35 -> 10*
       42 -> 31*
       61 -> 64*
       63 -> 37*
       70 -> 39*
     problem:
      
     Qed