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