1.98/1.55	MAYBE
1.98/1.55	
1.98/1.55	Proof:
1.98/1.55	ConCon could not decide confluence of the system.
1.98/1.55	\cite{ALS94}, Theorem 4.1 does not apply.
1.98/1.55	This system is of type 3 or smaller.
1.98/1.55	This system is strongly deterministic.
1.98/1.55	This system is of type 3 or smaller.
1.98/1.55	This system is deterministic.
1.98/1.55	This system is non-terminating.
1.98/1.55	Call external tool:
1.98/1.55	./ttt2.sh
1.98/1.55	Input:
1.98/1.55	(VAR x y)
1.98/1.55	(RULES
1.98/1.55	  pin(x) -> pout(g(x))
1.98/1.55	  ?1(pout(g(y)), x) -> pout(f(y))
1.98/1.55	  pin(x) -> ?1(pin(x), x)
1.98/1.55	)
1.98/1.55	
1.98/1.55	 Containment Processor: loop length: 1
1.98/1.55	                        terms:
1.98/1.55	                         pin(x)
1.98/1.55	                        context: ?1([],x)
1.98/1.55	                        substitution:
1.98/1.55	                         x -> x
1.98/1.55	  Qed
1.98/1.55	ConCon could not decide if this system is quasi-decreasing.
1.98/1.55	\cite{O02}, p. 214, Proposition 7.2.50 does not apply.
1.98/1.55	This system is of type 3 or smaller.
1.98/1.55	This system is deterministic.
1.98/1.55	This system is non-terminating.
1.98/1.55	Call external tool:
1.98/1.55	./ttt2.sh
1.98/1.55	Input:
1.98/1.55	(VAR x y)
1.98/1.55	(RULES
1.98/1.55	  pin(x) -> pout(g(x))
1.98/1.55	  ?1(pout(g(y)), x) -> pout(f(y))
1.98/1.55	  pin(x) -> ?1(pin(x), x)
1.98/1.55	)
1.98/1.55	
1.98/1.55	 Containment Processor: loop length: 1
1.98/1.55	                        terms:
1.98/1.56	                         pin(x)
1.98/1.56	                        context: ?1([],x)
1.98/1.56	                        substitution:
1.98/1.56	                         x -> x
1.98/1.56	  Qed
1.98/1.56	
1.98/1.57	EOF