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