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(y, x, y, z) -> G(z)
  F(x, y, z) -> ?1(x, x, y, z)
  G(A) -> F(A, B, A)
  e(x) -> f(x, x)
  f(x, y) -> x

 sorted: (order)
 0:?1(y,x,y,z) -> G(z)
   F(x,y,z) -> ?1(x,x,y,z)
   G(A()) -> F(A(),B(),A())
 1:e(x) -> f(x,x)
   f(x,y) -> x
 -----
 sorts
   [0>2, 0>4, 2>3, 2>5, 4>5]
 sort attachment (strict)
   ?1 : 2 x 2 x 2 x 4 -> 0
   G : 4 -> 0
   F : 2 x 2 x 4 -> 0
   A : 5
   B : 3
   e : 1 -> 1
   f : 1 x 1 -> 1
 -----
 0:?1(y,x,y,z) -> G(z)
   F(x,y,z) -> ?1(x,x,y,z)
   G(A()) -> F(A(),B(),A())
   Church Rosser Transformation Processor (kb):
    ?1(y,x,y,z) -> G(z)
    F(x,y,z) -> ?1(x,x,y,z)
    G(A()) -> F(A(),B(),A())
    critical peaks: joinable
     DP Processor:
      DPs:
       ?1#(y,x,y,z) -> G#(z)
       F#(x,y,z) -> ?1#(x,x,y,z)
       G#(A()) -> F#(A(),B(),A())
      TRS:
       ?1(y,x,y,z) -> G(z)
       F(x,y,z) -> ?1(x,x,y,z)
       G(A()) -> F(A(),B(),A())
      EDG Processor:
       DPs:
        ?1#(y,x,y,z) -> G#(z)
        F#(x,y,z) -> ?1#(x,x,y,z)
        G#(A()) -> F#(A(),B(),A())
       TRS:
        ?1(y,x,y,z) -> G(z)
        F(x,y,z) -> ?1(x,x,y,z)
        G(A()) -> F(A(),B(),A())
       graph:
        F#(x,y,z) -> ?1#(x,x,y,z) -> ?1#(y,x,y,z) -> G#(z)
        G#(A()) -> F#(A(),B(),A()) -> F#(x,y,z) -> ?1#(x,x,y,z)
        ?1#(y,x,y,z) -> G#(z) -> G#(A()) -> F#(A(),B(),A())
       Bounds Processor:
        bound: 0
        enrichment: top-dp
        automaton:
         final states: {8}
         transitions:
          B0() -> 10*
          A0() -> 9*
          F{#,0}(9,10,9) -> 8*
          ?1{#,0}(9,9,10,9) -> 8*
        problem:
         DPs:
          ?1#(y,x,y,z) -> G#(z)
          F#(x,y,z) -> ?1#(x,x,y,z)
         TRS:
          ?1(y,x,y,z) -> G(z)
          F(x,y,z) -> ?1(x,x,y,z)
          G(A()) -> F(A(),B(),A())
        SCC Processor:
         #sccs: 0
         #rules: 0
         #arcs: 3/4
         
   
   
   1:e(x) -> f(x,x)
     f(x,y) -> x
     Church Rosser Transformation Processor (kb):
      e(x) -> f(x,x)
      f(x,y) -> x
      critical peaks: joinable
       Matrix Interpretation Processor: dim=1
        
        interpretation:
         [e](x0) = 3x0 + 4,
         
         [f](x0, x1) = x0 + 2x1
        orientation:
         e(x) = 3x + 4 >= 3x = f(x,x)
         
         f(x,y) = x + 2y >= x = x
        problem:
         f(x,y) -> x
        Matrix Interpretation Processor: dim=1
         
         interpretation:
          [f](x0, x1) = 4x0 + 2x1 + 4
         orientation:
          f(x,y) = 4x + 2y + 4 >= x = x
         problem:
          
         Qed