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(z, x, y, z) -> x ?2(z, x, y) -> ?1(g(y), x, y, z) f(x, y) -> ?2(g(x), x, y) ?3(c, x) -> c g(x) -> ?3(d, x) Church Rosser Transformation Processor (kb): ?1(z,x,y,z) -> x ?2(z,x,y) -> ?1(g(y),x,y,z) f(x,y) -> ?2(g(x),x,y) ?3(c(),x) -> c() g(x) -> ?3(d(),x) critical peaks: joinable Matrix Interpretation Processor: dim=1 interpretation: [c] = 0, [?2](x0, x1, x2) = 2x0 + 2x1 + 6x2 + 5, [f](x0, x1) = 4x0 + 6x1 + 5, [?3](x0, x1) = 4x0 + x1, [?1](x0, x1, x2, x3) = 2x0 + x1 + 4x2 + 2x3 + 5, [d] = 0, [g](x0) = x0 orientation: ?1(z,x,y,z) = x + 4y + 4z + 5 >= x = x ?2(z,x,y) = 2x + 6y + 2z + 5 >= x + 6y + 2z + 5 = ?1(g(y),x,y,z) f(x,y) = 4x + 6y + 5 >= 4x + 6y + 5 = ?2(g(x),x,y) ?3(c(),x) = x >= 0 = c() g(x) = x >= x = ?3(d(),x) problem: ?2(z,x,y) -> ?1(g(y),x,y,z) f(x,y) -> ?2(g(x),x,y) ?3(c(),x) -> c() g(x) -> ?3(d(),x) Matrix Interpretation Processor: dim=1 interpretation: [c] = 0, [?2](x0, x1, x2) = x0 + 2x1 + 3x2 + 3, [f](x0, x1) = 5x0 + 3x1 + 4, [?3](x0, x1) = 2x0 + 2x1, [?1](x0, x1, x2, x3) = x0 + 2x1 + x2 + x3 + 2, [d] = 0, [g](x0) = 2x0 orientation: ?2(z,x,y) = 2x + 3y + z + 3 >= 2x + 3y + z + 2 = ?1(g(y),x,y,z) f(x,y) = 5x + 3y + 4 >= 4x + 3y + 3 = ?2(g(x),x,y) ?3(c(),x) = 2x >= 0 = c() g(x) = 2x >= 2x = ?3(d(),x) problem: ?3(c(),x) -> c() g(x) -> ?3(d(),x) Matrix Interpretation Processor: dim=1 interpretation: [c] = 4, [?3](x0, x1) = 2x0 + 4x1, [d] = 0, [g](x0) = 5x0 orientation: ?3(c(),x) = 4x + 8 >= 4 = c() g(x) = 5x >= 4x = ?3(d(),x) problem: g(x) -> ?3(d(),x) Matrix Interpretation Processor: dim=1 interpretation: [?3](x0, x1) = x0 + x1, [d] = 0, [g](x0) = x0 + 1 orientation: g(x) = x + 1 >= x = ?3(d(),x) problem: Qed