3.83/1.57	YES
3.83/1.57	
3.83/1.57	Proof:
3.83/1.57	This system is confluent.
3.83/1.57	By \cite{ALS94}, Theorem 4.1.
3.83/1.57	This system is of type 3 or smaller.
3.83/1.57	This system is strongly deterministic.
3.83/1.57	This system is quasi-decreasing.
3.83/1.57	By \cite{O02}, p. 214, Proposition 7.2.50.
3.83/1.57	This system is of type 3 or smaller.
3.83/1.57	This system is deterministic.
3.83/1.57	System R transformed to optimized U(R).
3.83/1.57	This system is terminating.
3.83/1.57	Call external tool:
3.83/1.57	./ttt2.sh
3.83/1.57	Input:
3.83/1.57	  f(g(x)) -> ?1(x, x)
3.83/1.57	  ?1(a, x) -> b
3.83/1.57	  g(x) -> ?2(x, x)
3.83/1.57	  ?2(c, x) -> c
3.83/1.57	
3.83/1.57	 Polynomial Interpretation Processor:
3.83/1.57	  dimension: 1
3.83/1.57	  interpretation:
3.83/1.57	   [c] = 4,
3.83/1.57	   
3.83/1.57	   [?2](x0, x1) = 2x0 + x1,
3.83/1.57	   
3.83/1.57	   [b] = 0,
3.83/1.57	   
3.83/1.57	   [a] = 0,
3.83/1.57	   
3.83/1.57	   [?1](x0, x1) = -2x0 + 3x0x0 + 2x1x1 + 2,
3.83/1.57	   
3.83/1.57	   [f](x0) = x0x0 + 2,
3.83/1.57	   
3.83/1.57	   [g](x0) = 4x0 + 5x0x0 + 1
3.83/1.57	  orientation:
3.83/1.57	   f(g(x)) = 8x + 26x*x + 40x*x*x + 25x*x*x*x + 3 >= -2x + 5x*x + 2 = ?1(x,x)
3.83/1.57	   
3.83/1.57	   ?1(a(),x) = 2x*x + 2 >= 0 = b()
3.83/1.57	   
3.83/1.57	   g(x) = 4x + 5x*x + 1 >= 3x = ?2(x,x)
3.83/1.57	   
3.83/1.57	   ?2(c(),x) = x + 8 >= 4 = c()
3.83/1.57	  problem:
3.83/1.57	   
3.83/1.57	  Qed
3.83/1.57	All 1 critical pairs are joinable.
3.83/1.57	Overlap: (rule1: f(g(y)) -> b <= y = a, rule2: g(z) -> c <= z = c, pos: 1, mgu: {(z,y)})
3.83/1.57	CP: f(c) = b <= y = a, y = c
3.83/1.58	This critical pair is unfeasible.
3.83/1.58	
3.83/1.59	EOF