0.00/0.83	YES
0.00/0.83	
0.00/0.83	Problem:
0.00/0.83	f(x, x') -> g(y, y) <= x = y, x' = y
0.00/0.83	h(x, x', x'') -> c() <= x = y, x' = y, x'' = y
0.00/0.83	
0.00/0.83	Proof:
0.00/0.83	This system is confluent.
0.00/0.83	By \cite{ALS94}, Theorem 4.1.
0.00/0.83	This system is of type 3 or smaller.
0.00/0.83	This system is strongly deterministic.
0.00/0.83	All 0 critical pairs are joinable.
0.00/0.83	This system is quasi-decreasing.
0.00/0.83	By \cite{A14}, Theorem 11.5.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	System R transformed to V(R) + Emb.
0.00/0.83	This system is terminating.
0.00/0.83	Call external tool:
0.00/0.83	./ttt2.sh
0.00/0.83	Input:
0.00/0.83	  f(x, x') -> g(x', x')
0.00/0.83	  f(x, x') -> x'
0.00/0.83	  f(x, x') -> x
0.00/0.83	  h(x, x', x'') -> c()
0.00/0.83	  h(x, x', x'') -> x''
0.00/0.83	  h(x, x', x'') -> x'
0.00/0.83	  h(x, x', x'') -> x
0.00/0.83	  h(x, y, z) -> x
0.00/0.83	  h(x, y, z) -> y
0.00/0.83	  h(x, y, z) -> z
0.00/0.83	  g(x, y) -> x
0.00/0.83	  g(x, y) -> y
0.00/0.83	  f(x, y) -> x
0.00/0.83	  f(x, y) -> y
0.00/0.83	
0.00/0.83	 Polynomial Interpretation Processor:
0.00/0.83	  dimension: 1
0.00/0.83	  interpretation:
0.00/0.83	   [c] = 0,
0.00/0.83	   
0.00/0.83	   [h](x0, x1, x2) = 2x0 + x1 + 2x2 + 6x0x0 + x2x2 + 1,
0.00/0.83	   
0.00/0.83	   [g](x0, x1) = x0 + 2x1 + 2,
0.00/0.83	   
0.00/0.83	   [f](x0, x1) = 2x0 + 4x1 + x0x0 + 5
0.00/0.83	  orientation:
0.00/0.83	   f(x,x') = 2x + x*x + 4x' + 5 >= 3x' + 2 = g(x',x')
0.00/0.83	   
0.00/0.83	   f(x,x') = 2x + x*x + 4x' + 5 >= x' = x'
0.00/0.83	   
0.00/0.83	   f(x,x') = 2x + x*x + 4x' + 5 >= x = x
0.00/0.83	   
0.00/0.83	   h(x,x',x'') = 2x + 6x*x + x' + 2x'' + x''*x'' + 1 >= 0 = c()
0.00/0.83	   
0.00/0.83	   h(x,x',x'') = 2x + 6x*x + x' + 2x'' + x''*x'' + 1 >= x'' = x''
0.00/0.83	   
0.00/0.83	   h(x,x',x'') = 2x + 6x*x + x' + 2x'' + x''*x'' + 1 >= x' = x'
0.00/0.83	   
0.00/0.83	   h(x,x',x'') = 2x + 6x*x + x' + 2x'' + x''*x'' + 1 >= x = x
0.00/0.83	   
0.00/0.83	   h(x,y,z) = 2x + 6x*x + y + 2z + z*z + 1 >= x = x
0.00/0.83	   
0.00/0.83	   h(x,y,z) = 2x + 6x*x + y + 2z + z*z + 1 >= y = y
0.00/0.83	   
0.00/0.83	   h(x,y,z) = 2x + 6x*x + y + 2z + z*z + 1 >= z = z
0.00/0.83	   
0.00/0.83	   g(x,y) = x + 2y + 2 >= x = x
0.00/0.83	   
0.00/0.83	   g(x,y) = x + 2y + 2 >= y = y
0.00/0.83	   
0.00/0.83	   f(x,y) = 2x + x*x + 4y + 5 >= x = x
0.00/0.83	   
0.00/0.83	   f(x,y) = 2x + x*x + 4y + 5 >= y = y
0.00/0.83	  problem:
0.00/0.83	   
0.00/0.83	  Qed
0.00/0.83	
0.00/0.91	EOF