1.30/1.08	MAYBE
1.30/1.08	
1.30/1.08	Proof:
1.30/1.08	ConCon could not decide confluence of the system.
1.30/1.08	\cite{ALS94}, Theorem 4.1 does not apply.
1.30/1.08	This system is of type 3 or smaller.
1.30/1.08	This system is strongly deterministic.
1.30/1.08	This system is of type 3 or smaller.
1.30/1.08	This system is deterministic.
1.30/1.08	This system is non-terminating.
1.30/1.08	Call external tool:
1.30/1.08	./ttt2.sh
1.30/1.08	Input:
1.30/1.08	  f(x) -> b
1.30/1.08	  f(x) -> x
1.30/1.08	  f(x) -> f(x)
1.30/1.08	  a -> f(a)
1.30/1.08	  f(x) -> x
1.30/1.08	
1.30/1.08	 Containment Processor: loop length: 1
1.30/1.08	                        terms:
1.30/1.08	                         f(x)
1.30/1.08	                        context: []
1.30/1.09	                        substitution:
1.30/1.09	                         x -> x
1.30/1.09	  Qed
1.30/1.09	ConCon could not decide if this system is quasi-decreasing.
1.30/1.09	\cite{A14}, Theorem 11.5.9 does not apply.
1.30/1.09	This system is of type 3 or smaller.
1.30/1.09	This system is deterministic.
1.30/1.09	This system is non-terminating.
1.30/1.09	Call external tool:
1.30/1.09	./ttt2.sh
1.30/1.09	Input:
1.30/1.09	  f(x) -> b
1.30/1.09	  f(x) -> x
1.30/1.09	  f(x) -> f(x)
1.30/1.09	  a -> f(a)
1.30/1.09	  f(x) -> x
1.30/1.09	
1.30/1.09	 Containment Processor: loop length: 1
1.30/1.09	                        terms:
1.30/1.09	                         f(x)
1.30/1.09	                        context: []
1.30/1.09	                        substitution:
1.30/1.09	                         x -> x
1.30/1.09	  Qed
1.30/1.09	
1.30/1.09	EOF