2.52/1.23	MAYBE
2.52/1.23	
2.52/1.23	Proof:
2.52/1.23	ConCon could not decide confluence of the system.
2.52/1.23	\cite{ALS94}, Theorem 4.1 does not apply.
2.52/1.23	This system is of type 3 or smaller.
2.52/1.23	This system is strongly deterministic.
2.52/1.23	This system is quasi-decreasing.
2.52/1.23	By \cite{A14}, Theorem 11.5.9.
2.52/1.23	This system is of type 3 or smaller.
2.52/1.23	This system is deterministic.
2.52/1.23	System R transformed to V(R) + Emb.
2.52/1.23	This system is terminating.
2.52/1.23	Call external tool:
2.52/1.23	./ttt2.sh
2.52/1.23	Input:
2.52/1.23	  a -> c
2.52/1.23	  a -> d
2.52/1.23	  f(x) -> x
2.52/1.23	  f(x) -> d
2.52/1.23	  f(x) -> x
2.52/1.23	
2.52/1.23	 Polynomial Interpretation Processor:
2.52/1.23	  dimension: 1
2.52/1.23	  interpretation:
2.52/1.23	   [f](x0) = 2x0 + 4,
2.52/1.23	   
2.52/1.23	   [d] = 0,
2.52/1.23	   
2.52/1.23	   [c] = 0,
2.52/1.23	   
2.52/1.23	   [a] = 4
2.52/1.23	  orientation:
2.52/1.23	   a() = 4 >= 0 = c()
2.52/1.23	   
2.52/1.23	   a() = 4 >= 0 = d()
2.52/1.23	   
2.52/1.23	   f(x) = 2x + 4 >= x = x
2.52/1.23	   
2.52/1.23	   f(x) = 2x + 4 >= 0 = d()
2.52/1.23	  problem:
2.52/1.23	   
2.52/1.23	  Qed
2.52/1.23	This critical pair is not trivial.
2.52/1.23	
2.52/1.25	EOF