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