1.77/1.03	MAYBE
1.77/1.03	
1.77/1.04	Proof:
1.77/1.04	ConCon could not decide confluence of the system.
1.77/1.04	\cite{ALS94}, Theorem 4.1 does not apply.
1.77/1.04	This system is of type 3 or smaller.
1.77/1.04	This system is strongly deterministic.
1.77/1.04	This system is of type 3 or smaller.
1.77/1.04	This system is deterministic.
1.77/1.04	This system is non-terminating.
1.77/1.04	Call external tool:
1.77/1.04	./ttt2.sh
1.77/1.04	Input:
1.77/1.04	  f(b, x) -> b
1.77/1.04	  g(x, a) -> ?2(f(x, b), x)
1.77/1.04	  ?2(b, x) -> d
1.77/1.04	  g(a, x) -> ?1(f(x, a), x)
1.77/1.04	  ?1(a, x) -> c
1.77/1.04	  f(a, x) -> a
1.77/1.04	  c -> c
1.77/1.04	
1.77/1.04	 Containment Processor: loop length: 1
1.77/1.04	                        terms:
1.77/1.04	                         c()
1.77/1.04	                        context: []
1.77/1.04	                        substitution:
1.77/1.04	                         
1.77/1.04	  Qed
1.77/1.04	ConCon could not decide if this system is quasi-decreasing.
1.77/1.04	\cite{O02}, p. 214, Proposition 7.2.50 does not apply.
1.77/1.04	This system is of type 3 or smaller.
1.77/1.04	This system is deterministic.
1.77/1.04	This system is non-terminating.
1.77/1.04	Call external tool:
1.77/1.04	./ttt2.sh
1.77/1.04	Input:
1.77/1.04	  f(b, x) -> b
1.77/1.04	  g(x, a) -> ?2(f(x, b), x)
1.77/1.04	  ?2(b, x) -> d
1.77/1.04	  g(a, x) -> ?1(f(x, a), x)
1.77/1.04	  ?1(a, x) -> c
1.77/1.04	  f(a, x) -> a
1.77/1.04	  c -> c
1.77/1.04	
1.77/1.04	 Containment Processor: loop length: 1
1.77/1.04	                        terms:
1.77/1.04	                         c()
1.77/1.04	                        context: []
1.77/1.04	                        substitution:
1.77/1.04	                         
1.77/1.04	  Qed
1.77/1.04	
1.77/1.06	EOF