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) -> G(x)
  F(x, y) -> ?1(x, x, y)
  a -> b

 sorted: (order)
 0:?1(y,x,y) -> G(x)
   F(x,y) -> ?1(x,x,y)
 1:a() -> b()
 -----
 sorts
   [0>1, 1>2, 2>5, 3>4]
 sort attachment (strict)
   ?1 : 5 x 5 x 5 -> 1
   G : 5 -> 2
   F : 5 x 5 -> 0
   a : 3
   b : 4
 -----
 0:?1(y,x,y) -> G(x)
   F(x,y) -> ?1(x,x,y)
   Church Rosser Transformation Processor (kb):
    ?1(y,x,y) -> G(x)
    F(x,y) -> ?1(x,x,y)
    critical peaks: joinable
     Matrix Interpretation Processor: dim=1
      
      interpretation:
       [G](x0) = x0,
       
       [?1](x0, x1, x2) = x0 + x1 + x2 + 2,
       
       [F](x0, x1) = 2x0 + 4x1 + 3
      orientation:
       ?1(y,x,y) = x + 2y + 2 >= x = G(x)
       
       F(x,y) = 2x + 4y + 3 >= 2x + y + 2 = ?1(x,x,y)
      problem:
       
      Qed
 
 
 1:a() -> b()
   Uncurry Processor:
    a() -> b()
    Ground Confluence Processor:
     confluent by decision procedure.
 
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.