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