0.00/0.82	YES
0.00/0.82	
0.00/0.82	Problem:
0.00/0.82	f(x) -> x <= x = a()
0.00/0.82	g(x) -> C() <= A() = B()
0.00/0.82	A() -> B()
0.00/0.82	
0.00/0.82	Proof:
0.00/0.82	This system is confluent.
0.00/0.82	By \cite{ALS94}, Theorem 4.1.
0.00/0.82	This system is of type 3 or smaller.
0.00/0.82	This system is strongly deterministic.
0.00/0.82	All 0 critical pairs are joinable.
0.00/0.82	This system is quasi-decreasing.
0.00/0.82	By \cite{A14}, Theorem 11.5.9.
0.00/0.82	This system is of type 3 or smaller.
0.00/0.82	This system is deterministic.
0.00/0.82	System R transformed to V(R) + Emb.
0.00/0.82	This system is terminating.
0.00/0.82	Call external tool:
0.00/0.82	./ttt2.sh
0.00/0.82	Input:
0.00/0.82	  f(x) -> x
0.00/0.82	  g(x) -> C()
0.00/0.82	  g(x) -> A()
0.00/0.82	  A() -> B()
0.00/0.82	  g(x) -> x
0.00/0.82	  f(x) -> x
0.00/0.82	
0.00/0.82	 Polynomial Interpretation Processor:
0.00/0.82	  dimension: 1
0.00/0.82	  interpretation:
0.00/0.82	   [B] = 0,
0.00/0.82	   
0.00/0.82	   [A] = 2,
0.00/0.82	   
0.00/0.82	   [C] = 0,
0.00/0.82	   
0.00/0.82	   [g](x0) = 2x0 + 3,
0.00/0.82	   
0.00/0.82	   [f](x0) = x0 + x0x0 + 2
0.00/0.82	  orientation:
0.00/0.82	   f(x) = x + x*x + 2 >= x = x
0.00/0.82	   
0.00/0.82	   g(x) = 2x + 3 >= 0 = C()
0.00/0.82	   
0.00/0.82	   g(x) = 2x + 3 >= 2 = A()
0.00/0.82	   
0.00/0.82	   A() = 2 >= 0 = B()
0.00/0.82	   
0.00/0.82	   g(x) = 2x + 3 >= x = x
0.00/0.82	  problem:
0.00/0.82	   
0.00/0.82	  Qed
0.00/0.82	
0.00/0.85	EOF