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