YES

Problem:
 strict:
  f(g(f(x))) -> f(g(g(g(f(x)))))
 weak:
  g(x) -> g(g(x))
  g(x) -> g(g(f(g(g(x)))))
  f(x) -> g(g(f(g(g(x)))))

Proof:
 Arctic Interpretation Processor:
  dimension: 3
  interpretation:
             [0  -& 0 ]  
   [g](x0) = [0  -& 2 ]x0
             [-& -& -&]  ,
   
             [0 0 2]  
   [f](x0) = [0 0 3]x0
             [0 0 1]  
  orientation:
                [2 2 3]     [0 0 2]                    
   f(g(f(x))) = [2 2 3]x >= [0 0 2]x = f(g(g(g(f(x)))))
                [2 2 3]     [0 0 2]                    
   
          [0  -& 0 ]     [0  -& 0 ]           
   g(x) = [0  -& 2 ]x >= [0  -& 0 ]x = g(g(x))
          [-& -& -&]     [-& -& -&]           
   
          [0  -& 0 ]     [0  -& 0 ]                    
   g(x) = [0  -& 2 ]x >= [0  -& 0 ]x = g(g(f(g(g(x)))))
          [-& -& -&]     [-& -& -&]                    
   
          [0 0 2]     [0  -& 0 ]                    
   f(x) = [0 0 3]x >= [0  -& 0 ]x = g(g(f(g(g(x)))))
          [0 0 1]     [-& -& -&]                    
  problem:
   strict:
    
   weak:
    g(x) -> g(g(x))
    g(x) -> g(g(f(g(g(x)))))
    f(x) -> g(g(f(g(g(x)))))
  Qed