YES

Proof:
This system is confluent.
By \cite{GNG13}, Theorem 9.
This system is deterministic.
This system is weakly left-linear.
System R transformed to optimized U(R).
This system is not orthogonal.
Call external tool:
csi - trs 30
Input:
  ?1(b, x) -> c
  f(x) -> ?1(a, x)
  g(x, x) -> g(f(a), f(b))

 Church Rosser Transformation Processor (kb):
  ?1(b(),x) -> c()
  f(x) -> ?1(a(),x)
  g(x,x) -> g(f(a()),f(b()))
  critical peaks: joinable
   Matrix Interpretation Processor: dim=2
    
    interpretation:
           [0]
     [a] = [0],
     
                    [2 1]     [1 0]     [0]
     [?1](x0, x1) = [0 0]x0 + [0 0]x1 + [3],
     
                    [0]
     [f](x0) = x0 + [3],
     
                   [1 0]     [2 0]     [0]
     [g](x0, x1) = [0 0]x0 + [1 0]x1 + [1],
     
           [0]
     [b] = [1],
     
           [0]
     [c] = [0]
    orientation:
                 [1 0]    [1]    [0]      
     ?1(b(),x) = [0 0]x + [3] >= [0] = c()
     
                [0]    [1 0]    [0]            
     f(x) = x + [3] >= [0 0]x + [3] = ?1(a(),x)
     
              [3 0]    [0]    [0]                   
     g(x,x) = [1 0]x + [1] >= [1] = g(f(a()),f(b()))
    problem:
     f(x) -> ?1(a(),x)
     g(x,x) -> g(f(a()),f(b()))
    Bounds Processor:
     bound: 1
     enrichment: match
     automaton:
      final states: {4,1}
      transitions:
       a1() -> 9*,3,8
       ?10(9,2) -> 1*
       ?10(3,5) -> 6*
       ?10(9,3) -> 7*
       ?10(3,2) -> 1*
       ?10(3,3) -> 7*
       ?10(9,9) -> 7*
       ?10(9,5) -> 6*
       ?10(3,9) -> 7*
       f60() -> 2*
       ?11(9,9) -> 7*
       ?11(8,3) -> 7*
       ?11(8,9) -> 7*
       ?11(9,3) -> 7*
       ?11(9,5) -> 6*
       ?11(8,5) -> 6*
       b0() -> 5*
       f0(5) -> 6*
       f0(3) -> 7*
       f0(9) -> 7*
       g0(7,6) -> 4*
     problem:
      
     Qed