0.00/0.82	YES
0.00/0.82	
0.00/0.82	Problem:
0.00/0.83	f(x, y) -> x <= g(x) = z, g(y) = z
0.00/0.83	g(x) -> c() <= d() = c()
0.00/0.83	
0.00/0.83	Proof:
0.00/0.83	This system is confluent.
0.00/0.83	By \cite{GNG13}, Theorem 9.
0.00/0.83	This system is of type 3 or smaller.
0.00/0.83	This system is deterministic.
0.00/0.83	This system is weakly left-linear.
0.00/0.83	System R transformed to optimized U(R).
0.00/0.83	This system is confluent.
0.00/0.83	Call external tool:
0.00/0.83	./csi.sh
0.00/0.83	Input:
0.00/0.83	  ?1(z, x, y, z) -> x
0.00/0.83	  ?2(z, x, y) -> ?1(g(y), x, y, z)
0.00/0.83	  f(x, y) -> ?2(g(x), x, y)
0.00/0.83	  ?3(c(), x) -> c()
0.00/0.83	  g(x) -> ?3(d(), x)
0.00/0.83	
0.00/0.83	 Church Rosser Transformation Processor (kb):
0.00/0.83	  ?1(z,x,y,z) -> x
0.00/0.83	  ?2(z,x,y) -> ?1(g(y),x,y,z)
0.00/0.83	  f(x,y) -> ?2(g(x),x,y)
0.00/0.83	  ?3(c(),x) -> c()
0.00/0.83	  g(x) -> ?3(d(),x)
0.00/0.83	  critical peaks: joinable
0.00/0.83	   Matrix Interpretation Processor: dim=1
0.00/0.83	    
0.00/0.83	    interpretation:
0.00/0.83	     [d] = 0,
0.00/0.83	     
0.00/0.83	     [?3](x0, x1) = x0 + x1,
0.00/0.83	     
0.00/0.83	     [c] = 0,
0.00/0.83	     
0.00/0.83	     [f](x0, x1) = 3x0 + 5x1 + 4,
0.00/0.83	     
0.00/0.83	     [g](x0) = x0 + 1,
0.00/0.83	     
0.00/0.83	     [?2](x0, x1, x2) = x0 + 2x1 + 5x2 + 2,
0.00/0.83	     
0.00/0.83	     [?1](x0, x1, x2, x3) = x0 + x1 + 4x2 + x3
0.00/0.83	    orientation:
0.00/0.83	     ?1(z,x,y,z) = x + 4y + 2z >= x = x
0.00/0.83	     
0.00/0.83	     ?2(z,x,y) = 2x + 5y + z + 2 >= x + 5y + z + 1 = ?1(g(y),x,y,z)
0.00/0.83	     
0.00/0.83	     f(x,y) = 3x + 5y + 4 >= 3x + 5y + 3 = ?2(g(x),x,y)
0.00/0.83	     
0.00/0.83	     ?3(c(),x) = x >= 0 = c()
0.00/0.83	     
0.00/0.83	     g(x) = x + 1 >= x = ?3(d(),x)
0.00/0.83	    problem:
0.00/0.83	     ?1(z,x,y,z) -> x
0.00/0.83	     ?3(c(),x) -> c()
0.00/0.83	    Matrix Interpretation Processor: dim=1
0.00/0.83	     
0.00/0.83	     interpretation:
0.00/0.83	      [?3](x0, x1) = 5x0 + 4x1 + 1,
0.00/0.83	      
0.00/0.83	      [c] = 6,
0.00/0.83	      
0.00/0.83	      [?1](x0, x1, x2, x3) = x0 + 2x1 + 2x2 + 7x3 + 1
0.00/0.83	     orientation:
0.00/0.83	      ?1(z,x,y,z) = 2x + 2y + 8z + 1 >= x = x
0.00/0.83	      
0.00/0.83	      ?3(c(),x) = 4x + 31 >= 6 = c()
0.00/0.83	     problem:
0.00/0.83	      
0.00/0.83	     Qed
0.00/0.83	
0.00/0.85	EOF