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