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