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()))
    DP Processor:
     DPs:
      g#(x,x) -> f#(b())
      g#(x,x) -> f#(a())
      g#(x,x) -> g#(f(a()),f(b()))
     TRS:
      f(x) -> ?1(a(),x)
      g(x,x) -> g(f(a()),f(b()))
     EDG Processor:
      DPs:
       g#(x,x) -> f#(b())
       g#(x,x) -> f#(a())
       g#(x,x) -> g#(f(a()),f(b()))
      TRS:
       f(x) -> ?1(a(),x)
       g(x,x) -> g(f(a()),f(b()))
      graph:
       g#(x,x) -> g#(f(a()),f(b())) -> g#(x,x) -> f#(b())
       g#(x,x) -> g#(f(a()),f(b())) -> g#(x,x) -> f#(a())
       g#(x,x) -> g#(f(a()),f(b())) -> g#(x,x) -> g#(f(a()),f(b()))
      SCC Processor:
       #sccs: 1
       #rules: 1
       #arcs: 3/9
       DPs:
        g#(x,x) -> g#(f(a()),f(b()))
       TRS:
        f(x) -> ?1(a(),x)
        g(x,x) -> g(f(a()),f(b()))
       Bounds Processor:
        bound: 0
        enrichment: match-dp
        automaton:
         final states: {1}
         transitions:
          ?10(4,2) -> 3*
          ?10(4,4) -> 5*
          b0() -> 2*
          a0() -> 4*
          f0(4) -> 5*
          f0(2) -> 3*
          g{#,0}(5,3) -> 1*
        problem:
         DPs:
          
         TRS:
          f(x) -> ?1(a(),x)
          g(x,x) -> g(f(a()),f(b()))
        Qed
This system is normal.
This system is of type 3 or smaller.
This system is right-stable.
This system is properly oriented.
This is an overlay system.
This system is not left-linear.
This system is conditional.