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