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