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:
      strict:
       e(x) -> f(x,x)
       f(x,y) -> x
      weak:
       
      critical peaks: 0
      Closedness Processor (*parallel*):
       strict:
        
       weak:
        
       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.