1.31/2.87	YES
1.31/2.87	
1.31/2.87	Proof:
1.31/2.87	This system is confluent.
1.31/2.87	By \cite{ALS94}, Theorem 4.1.
1.31/2.87	This system is of type 3 or smaller.
1.31/2.87	This system is strongly deterministic.
1.31/2.87	This system is quasi-decreasing.
1.31/2.87	By \cite{O02}, p. 214, Proposition 7.2.50.
1.31/2.87	This system is of type 3 or smaller.
1.31/2.87	This system is deterministic.
1.31/2.87	System R transformed to U(R).
1.31/2.87	This system is terminating.
1.31/2.87	Call external tool:
1.31/2.87	./ttt2.sh
1.31/2.87	Input:
1.31/2.87	  ?2(y, x, x', y) -> g(y, y)
1.31/2.87	  ?1(y, x, x') -> ?2(x', x, x', y)
1.31/2.87	  f(x, x') -> ?1(x, x, x')
1.31/2.87	  ?5(y, x, x', x'', y) -> c
1.31/2.87	  ?4(y, x, x', x'', y) -> ?5(x'', x, x', x'', y)
1.31/2.87	  ?3(y, x, x', x'') -> ?4(x', x, x', x'', y)
1.31/2.87	  h(x, x', x'') -> ?3(x, x, x', x'')
1.31/2.87	
1.31/2.87	 Polynomial Interpretation Processor:
1.31/2.87	  dimension: 1
1.31/2.87	  interpretation:
1.31/2.87	   [h](x0, x1, x2) = 5x0 + 2x1 + 5x2 + 5x1x1 + 3x2x2 + 6,
1.31/2.87	   
1.31/2.87	   [?3](x0, x1, x2, x3) = 4x0 + x1 + x2 + x2x2 + 2x3x3 + 5,
1.31/2.87	   
1.31/2.87	   [?4](x0, x1, x2, x3, x4) = x1 + x2 + 4x4 + x0x0 + 2x3x3 + 4,
1.31/2.87	   
1.31/2.87	   [c] = 0,
1.31/2.87	   
1.31/2.87	   [?5](x0, x1, x2, x3, x4) = x1 + x2 + 4x4 + x0x0 + x3x3 + 1,
1.31/2.87	   
1.31/2.87	   [f](x0, x1) = 7x0 + x1 + x0x0 + 6x1x1 + 7,
1.31/2.87	   
1.31/2.87	   [?1](x0, x1, x2) = 6x0 + x2 + x1x1 + 4x2x2 + 6,
1.31/2.87	   
1.31/2.87	   [g](x0, x1) = x0 + x1 + 3x0x0,
1.31/2.87	   
1.31/2.87	   [?2](x0, x1, x2, x3) = -3x0 + 2x2 + 6x3 + 4x0x0 + x1x1 + 4
1.31/2.87	  orientation:
1.31/2.87	   ?2(y,x,x',y) = x*x + 2x' + 3y + 4y*y + 4 >= 2y + 3y*y = g(y,y)
1.31/2.87	   
1.31/2.87	   ?1(y,x,x') = x*x + x' + 4x'*x' + 6y + 6 >= x*x + -1x' + 4x'*x' + 6y + 4 = ?2(x',x,x',y)
1.31/2.87	   
1.31/2.87	   f(x,x') = 7x + x*x + x' + 6x'*x' + 7 >= 6x + x*x + x' + 4x'*x' + 6 = ?1(x,x,x')
1.31/2.87	   
1.31/2.87	   ?5(y,x,x',x'',y) = x + x' + x''*x'' + 4y + y*y + 1 >= 0 = c()
1.31/2.87	   
1.31/2.87	   ?4(y,x,x',x'',y) = x + x' + 2x''*x'' + 4y + y*y + 4 >= x + x' + 2x''*x'' + 4y + 1 = ?5(x'',x,x',x'',y)
1.31/2.87	   
1.31/2.87	   ?3(y,x,x',x'') = x + x' + x'*x' + 2x''*x'' + 4y + 5 >= x + x' + x'*x' + 2x''*x'' + 4y + 4 = ?4(x',x,x',x'',y)
1.31/2.87	   
1.31/2.87	   h(x,x',x'') = 5x + 2x' + 5x'*x' + 5x'' + 3x''*x'' + 6 >= 5x + x' + x'*x' + 2x''*x'' + 5 = ?3(x,x,x',x'')
1.31/2.87	  problem:
1.31/2.87	   
1.31/2.87	  Qed
1.31/2.87	All 0 critical pairs are joinable.
1.31/2.87	
2.61/2.96	EOF