YES

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

Proof:
 Church Rosser Transformation Processor (critical pair closing system, Thm 2.11):
  f(f(g(x11,x13))) -> f(g(f(g(x11,x13)),f(g(x11,x13))))
  f(f(x14)) -> f(g(f(x14),f(x14)))
  critical peaks: joinable
  Matrix Interpretation Processor: dim=2
   
   interpretation:
                  [1 0]     [1 0]     [1]
    [g](x0, x1) = [0 0]x0 + [0 0]x1 + [0],
    
              [1 1]     [0]
    [f](x0) = [1 1]x0 + [2]
   orientation:
                       [2 0]      [2 0]      [4]    [2 0]      [2 0]      [3]                                    
    f(f(g(x11,x13))) = [2 0]x11 + [2 0]x13 + [6] >= [2 0]x11 + [2 0]x13 + [5] = f(g(f(g(x11,x13)),f(g(x11,x13))))
    
                [2 2]      [2]    [2 2]      [1]                      
    f(f(x14)) = [2 2]x14 + [4] >= [2 2]x14 + [3] = f(g(f(x14),f(x14)))
   problem:
    
   Qed