2.64/1.28	YES
2.64/1.28	
2.64/1.28	Proof:
2.64/1.28	This system is confluent.
2.64/1.28	By \cite{ALS94}, Theorem 4.1.
2.64/1.28	This system is of type 3 or smaller.
2.64/1.28	This system is strongly deterministic.
2.64/1.28	This system is quasi-decreasing.
2.64/1.28	By \cite{O02}, p. 214, Proposition 7.2.50.
2.64/1.28	This system is of type 3 or smaller.
2.64/1.28	This system is deterministic.
2.64/1.28	System R transformed to optimized U(R).
2.64/1.28	This system is terminating.
2.64/1.28	Call external tool:
2.64/1.28	./ttt2.sh
2.64/1.28	Input:
2.64/1.28	  f(x) -> ?1(a, x)
2.64/1.28	  ?1(x, x) -> a
2.64/1.28	  f(x) -> ?2(b, x)
2.64/1.28	  ?2(x, x) -> b
2.64/1.28	
2.64/1.29	 Polynomial Interpretation Processor:
2.64/1.29	  dimension: 1
2.64/1.29	  interpretation:
2.64/1.29	   [?2](x0, x1) = 2x0 + 2x1 + 7x0x0 + 1,
2.64/1.29	   
2.64/1.29	   [b] = 0,
2.64/1.29	   
2.64/1.29	   [?1](x0, x1) = 2x1 + 6x0x0 + 1,
2.64/1.29	   
2.64/1.29	   [a] = 0,
2.64/1.29	   
2.64/1.29	   [f](x0) = 6x0 + 2x0x0 + 6
2.64/1.29	  orientation:
2.64/1.29	   f(x) = 6x + 2x*x + 6 >= 2x + 1 = ?1(a(),x)
2.64/1.29	   
2.64/1.29	   ?1(x,x) = 2x + 6x*x + 1 >= 0 = a()
2.64/1.29	   
2.64/1.29	   f(x) = 6x + 2x*x + 6 >= 2x + 1 = ?2(b(),x)
2.64/1.29	   
2.64/1.29	   ?2(x,x) = 4x + 7x*x + 1 >= 0 = b()
2.64/1.30	  problem:
2.64/1.30	   
2.64/1.30	  Qed
2.64/1.30	All 2 critical pairs are joinable.
2.64/1.30	Overlap: (rule1: f(y) -> b <= b = y, rule2: f(z) -> a <= a = z, pos: ε, mgu: {(z,y)})
2.64/1.30	CP: a = b <= b = y, a = y
2.64/1.30	This critical pair is context-joinable.
2.64/1.30	Overlap: (rule1: f(y) -> a <= a = y, rule2: f(z) -> b <= b = z, pos: ε, mgu: {(z,y)})
2.64/1.30	CP: b = a <= a = y, b = y
2.64/1.30	This critical pair is context-joinable.
2.64/1.30	
2.90/1.32	EOF