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:
  f(x, x) -> a
  ?1(b, x) -> a
  g(x) -> ?1(g(x), x)
  a -> b
  b -> a

 sorted: (order)
 0:f(x,x) -> a()
   a() -> b()
   b() -> a()
 1:?1(b(),x) -> a()
   g(x) -> ?1(g(x),x)
   a() -> b()
   b() -> a()
 -----
 sorts
   [0>2, 0>4, 1>2, 1>3]
 sort attachment (strict)
   f : 4 x 4 -> 0
   a : 2
   ?1 : 1 x 3 -> 1
   b : 2
   g : 3 -> 1
 -----
 0:f(x,x) -> a()
   a() -> b()
   b() -> a()
   Church Rosser Transformation Processor (to relative problem):
    strict:
     f(x,x) -> a()
     a() -> b()
     b() -> a()
    weak:
     
    original problem:
     f(x,x) -> a()
     a() -> b()
     b() -> a()
    critical peaks: 
     Polynomial Interpretation Processor:
      dimension: 1
      interpretation:
       [a] = 0,
       
       [f](x0, x1) = x0 + x1x1 + 2,
       
       [b] = 0
      orientation:
       f(x,x) = x + x*x + 2 >= 0 = a()
       
       a() = 0 >= 0 = b()
       
       b() = 0 >= 0 = a()
      problem:
       strict:
        a() -> b()
        b() -> a()
       weak:
        
       original problem:
        f(x,x) -> a()
        a() -> b()
        b() -> a()
      KH confluence processor
       Split input TRS into two TRSs S and T:
       
       TRS S:
        a() -> b()
        b() -> a()
       
       TRS T:
        f(x,x) -> a()
       
       As established above, T/S is terminating.
       T is strongly non-overlapping on S and S is strongly non-overlapping on T
       
       Please install theorem prover 'Prover9' and 'Mace4' for handling more TRSs.
       
        All S-critical pairs are joinable.
       
       We have to check confluence of S.
       
       Church Rosser Transformation Processor:
        strict:
         a() -> b()
         b() -> a()
        weak:
         
        critical peaks: 0
        Closedness Processor (*strongly -- <=7 steps*):
         strict:
          
         weak:
          
         Qed
 
 
 1:?1(b(),x) -> a()
   g(x) -> ?1(g(x),x)
   a() -> b()
   b() -> a()
   Church Rosser Transformation Processor:
    strict:
     
    weak:
     
    critical peaks: 1
     ?1(a(),x) <-3|0[]- ?1(b(),x) -0|[]-> a()
    Shift Processor lab=left (dd) (force):
     strict:
      ?1(b(),x) -> ?1(a(),x)
      ?1(b(),x) -> a()
      ?1(a(),x) -> ?1(b(),x)
      ?1(b(),x) -> a()
     weak:
      ?1(b(),x) -> a()
      g(x) -> ?1(g(x),x)
      a() -> b()
      b() -> a()
     Shift Processor (ldh) lab=left (force):
      strict:
       
      weak:
       
      Rule Labeling Processor:
       strict:
        
       weak:
        
       rule labeling (right):
        ?1(b(),x) -> a(): 0
        g(x) -> ?1(g(x),x): 0
        a() -> b(): 0
        b() -> a(): 1
       Rule Labeling Processor:
        strict:
         
        weak:
         
        rule labeling (left):
         ?1(b(),x) -> a(): 0
         g(x) -> ?1(g(x),x): 0
         a() -> b(): 0
         b() -> a(): 0
        Decreasing Processor:
         The following diagrams are decreasing:
         peak:
          ?1(a(),x) <-3|0[==0,==1,=?1]- ?1(b(),x) -0|[==0,==1,>=0]-> a()
         joins (1):
          ?1(a(),x) -2|0[==0,==1,>=0]-> ?1(b(),x) -0|[==0,==1,>=0]-> a()
          
         Qed
  
This system is not normal.
This system is oriented.
This system is of type 3 or smaller.
This system is not right-stable.
This system is conditional.