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