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: 5
     enrichment: match
     automaton:
      final states: {2,1}
      transitions:
       g{1,2}(70) -> 71*
       g{1,2}(137) -> 138*
       g{1,2}(77) -> 78*
       g{1,2}(72) -> 73*
       g{1,2}(42) -> 43*
       g{1,2}(94) -> 95*
       g{1,2}(79) -> 80*
       g{1,2}(136) -> 137*
       g{1,2}(71) -> 72*
       g{1,2}(41) -> 42*
       g{1,2}(93) -> 94*
       g{1,2}(78) -> 79*
       g{1,2}(43) -> 44*
       g{1,2}(135) -> 136*
       g{1,2}(95) -> 96*
       f{1,2}(75) -> 76*
       f{1,2}(40) -> 41*
       f{1,2}(132) -> 133*
       f{1,2}(97) -> 98*
       f{1,2}(92) -> 93*
       f{1,2}(67) -> 68*
       f{1,2}(134) -> 135*
       f{1,2}(74) -> 75*
       f{1,2}(69) -> 70*
       f{1,2}(39) -> 40*
       f{1,2}(101) -> 102*
       f{1,2}(91) -> 92*
       f{1,2}(76) -> 77*
       f{1,2}(133) -> 134*
       f{1,2}(103) -> 104*
       f{1,2}(68) -> 69*
       f{1,2}(38) -> 39*
       f{1,2}(105) -> 106*
       f{1,2}(90) -> 91*
       g{1,3}(217) -> 218*
       g{1,3}(157) -> 158*
       g{1,3}(147) -> 148*
       g{1,3}(117) -> 118*
       g{1,3}(179) -> 180*
       g{1,3}(169) -> 170*
       g{1,3}(119) -> 120*
       g{1,3}(216) -> 217*
       g{1,3}(171) -> 172*
       g{1,3}(156) -> 157*
       g{1,3}(146) -> 147*
       g{1,3}(178) -> 179*
       g{1,3}(148) -> 149*
       g{1,3}(118) -> 119*
       g{1,3}(215) -> 216*
       g{1,3}(180) -> 181*
       g{1,3}(170) -> 171*
       g{1,3}(155) -> 156*
       f{1,3}(212) -> 213*
       f{1,3}(177) -> 178*
       f{1,3}(167) -> 168*
       f{1,3}(152) -> 153*
       f{1,3}(214) -> 215*
       f{1,3}(154) -> 155*
       f{1,3}(144) -> 145*
       f{1,3}(114) -> 115*
       f{1,3}(176) -> 177*
       f{1,3}(166) -> 167*
       f{1,3}(141) -> 142*
       f{1,3}(121) -> 122*
       f{1,3}(116) -> 117*
       f{1,3}(213) -> 214*
       f{1,3}(168) -> 169*
       f{1,3}(153) -> 154*
       f{1,3}(143) -> 144*
       f{1,3}(175) -> 176*
       f{1,3}(150) -> 151*
       f{1,3}(145) -> 146*
       f{1,3}(115) -> 116*
       g{1,4}(282) -> 283*
       g{1,4}(252) -> 253*
       g{1,4}(237) -> 238*
       g{1,4}(274) -> 275*
       g{1,4}(259) -> 260*
       g{1,4}(254) -> 255*
       g{1,4}(194) -> 195*
       g{1,4}(281) -> 282*
       g{1,4}(261) -> 262*
       g{1,4}(236) -> 237*
       g{1,4}(196) -> 197*
       g{1,4}(273) -> 274*
       g{1,4}(253) -> 254*
       g{1,4}(238) -> 239*
       g{1,4}(280) -> 281*
       g{1,4}(275) -> 276*
       g{1,4}(260) -> 261*
       g{1,4}(195) -> 196*
       f{1,4}(277) -> 278*
       f{1,4}(272) -> 273*
       f{1,4}(257) -> 258*
       f{1,4}(192) -> 193*
       f{1,4}(279) -> 280*
       f{1,4}(249) -> 250*
       f{1,4}(234) -> 235*
       f{1,4}(271) -> 272*
       f{1,4}(256) -> 257*
       f{1,4}(251) -> 252*
       f{1,4}(191) -> 192*
       f{1,4}(278) -> 279*
       f{1,4}(258) -> 259*
       f{1,4}(233) -> 234*
       f{1,4}(193) -> 194*
       f{1,4}(270) -> 271*
       f{1,4}(250) -> 251*
       f{1,4}(240) -> 241*
       f{1,4}(235) -> 236*
       f{1,0}(2) -> 1*
       f{1,0}(1) -> 1*
       g{1,5}(299) -> 300*
       g{1,5}(291) -> 292*
       g{1,5}(298) -> 299*
       g{1,5}(293) -> 294*
       g{1,5}(300) -> 301*
       g{1,5}(292) -> 293*
       g{1,0}(2) -> 2*
       g{1,0}(1) -> 2*
       f{1,5}(289) -> 290*
       f{1,5}(296) -> 297*
       f{1,5}(288) -> 289*
       f{1,5}(295) -> 296*
       f{1,5}(290) -> 291*
       f{1,5}(297) -> 298*
       g{1,1}(30) -> 31*
       g{1,1}(32) -> 33*
       g{1,1}(7) -> 8*
       g{1,1}(9) -> 10*
       g{1,1}(31) -> 32*
       g{1,1}(8) -> 9*
       f{1,1}(25) -> 26*
       f{1,1}(5) -> 6*
       f{1,1}(27) -> 28*
       f{1,1}(29) -> 30*
       f{1,1}(4) -> 5*
       f{1,1}(61) -> 62*
       f{1,1}(36) -> 37*
       f{1,1}(6) -> 7*
       f{1,1}(63) -> 64*
       f{1,1}(28) -> 29*
       1 -> 25*
       2 -> 4*
       7 -> 74*
       8 -> 38,36
       9 -> 27*
       10 -> 26,6,5,1
       26 -> 5*
       30 -> 101*
       31 -> 67,63
       32 -> 61*
       33 -> 26,6,1,5
       37 -> 5*
       41 -> 150*
       42 -> 121,97
       43 -> 105*
       44 -> 40,75,7,6
       62 -> 5*
       64 -> 5*
       70 -> 143*
       71 -> 114,90
       72 -> 103*
       73 -> 75,6,7
       78 -> 132*
       80 -> 29*
       94 -> 141*
       96 -> 75*
       98 -> 91*
       102 -> 39*
       104 -> 39*
       106 -> 39*
       117 -> 191*
       118 -> 240*
       119 -> 175*
       120 -> 151,144,77,76
       122 -> 115*
       136 -> 166*
       138 -> 102*
       142 -> 115*
       147 -> 152*
       149 -> 40*
       151 -> 144*
       156 -> 233*
       158 -> 151,144
       169 -> 256*
       170 -> 249*
       171 -> 212*
       172 -> 41*
       181 -> 134*
       197 -> 177*
       216 -> 277*
       218 -> 92,116
       236 -> 295*
       238 -> 270*
       239 -> 146*
       241 -> 234*
       255 -> 145*
       262 -> 214*
       276 -> 154*
       281 -> 288*
       283 -> 192*
       294 -> 194*
       301 -> 272*
     problem:
      
     Qed