6.34/2.49	MAYBE
6.34/2.49	
6.34/2.49	Proof:
6.34/2.49	ConCon could not decide confluence of the system.
6.34/2.49	\cite{ALS94}, Theorem 4.1 does not apply.
6.34/2.49	This system is of type 3 or smaller.
6.34/2.49	This system is strongly deterministic.
6.34/2.49	This system is of type 3 or smaller.
6.34/2.49	This system is deterministic.
6.34/2.49	This system is non-terminating.
6.34/2.49	Call external tool:
6.34/2.49	./ttt2.sh
6.34/2.49	Input:
6.34/2.49	(VAR x y z)
6.34/2.49	(RULES
6.34/2.49	  App(App(App(C, F), x), y) -> y
6.34/2.49	  App(App(App(C, T), x), y) -> x
6.34/2.49	  App(App(App(C, z), x), y) -> ?1(x, z, x, y)
6.34/2.49	  ?1(y, z, x, y) -> x
6.34/2.49	  App(App(App(S, x), y), z) -> App(App(x, z), App(y, z))
6.34/2.49	  App(I, x) -> x
6.34/2.49	  App(App(App(C, z), x), y) -> ?1(x, z, x, y)
6.34/2.49	  ?1(y, z, x, y) -> y
6.34/2.49	  App(App(K, x), y) -> x
6.34/2.49	)
6.34/2.49	
6.34/2.49	 Unfolding Processor:
6.34/2.49	  loop length: 3
6.34/2.49	  terms:
6.34/2.49	   App(App(App(S(),App(S(),x543)),App(App(C(),F()),x666)),App(App(S(),App(S(),x543)),
6.34/2.49	                                                              App(App(C(),F()),x666)))
6.34/2.49	   App(App(App(S(),x543),App(App(S(),App(S(),x543)),App(App(C(),F()),x666))),
6.34/2.49	       App(App(App(C(),F()),x666),App(App(S(),App(S(),x543)),App(App(C(),F()),x666))))
6.34/2.49	   App(App(x543,App(App(App(C(),F()),x666),App(App(S(),App(S(),x543)),App(App(C(),F()),x666)))),
6.34/2.49	       App(App(App(S(),App(S(),x543)),App(App(C(),F()),x666)),App(App(App(C(),F()),x666),
6.34/2.49	                                                                  App
6.34/2.49	                                                                  (App(S(),App(S(),x543)),
6.34/2.49	                                                                   App
6.34/2.49	                                                                   (App(C(),F()),x666)))))
6.34/2.49	  context:
6.34/2.49	   App(App(x543,App(App(App(C(),F()),x666),App(App(S(),App(S(),x543)),App(App(C(),F()),x666)))),[])
6.34/2.49	  substitution:
6.34/2.49	   x543 -> x543
6.34/2.49	   x666 -> x666
6.34/2.49	  Qed
6.34/2.49	ConCon could not decide if this system is quasi-decreasing.
6.34/2.49	\cite{O02}, p. 214, Proposition 7.2.50 does not apply.
6.34/2.49	This system is of type 3 or smaller.
6.34/2.49	This system is deterministic.
6.34/2.49	This system is non-terminating.
6.34/2.49	Call external tool:
6.34/2.49	./ttt2.sh
6.34/2.49	Input:
6.34/2.49	(VAR x y z)
6.34/2.49	(RULES
6.34/2.49	  App(App(App(C, F), x), y) -> y
6.34/2.49	  App(App(App(C, T), x), y) -> x
6.34/2.49	  App(App(App(C, z), x), y) -> ?1(x, z, x, y)
6.34/2.49	  ?1(y, z, x, y) -> x
6.34/2.49	  App(App(App(S, x), y), z) -> App(App(x, z), App(y, z))
6.34/2.49	  App(I, x) -> x
6.34/2.49	  App(App(App(C, z), x), y) -> ?1(x, z, x, y)
6.34/2.49	  ?1(y, z, x, y) -> y
6.34/2.49	  App(App(K, x), y) -> x
6.34/2.49	)
6.34/2.49	
6.34/2.49	 Unfolding Processor:
6.34/2.49	  loop length: 3
6.34/2.49	  terms:
6.34/2.49	   App(App(App(S(),App(S(),x543)),App(App(C(),F()),x666)),App(App(S(),App(S(),x543)),
6.34/2.49	                                                              App(App(C(),F()),x666)))
6.34/2.49	   App(App(App(S(),x543),App(App(S(),App(S(),x543)),App(App(C(),F()),x666))),
6.34/2.49	       App(App(App(C(),F()),x666),App(App(S(),App(S(),x543)),App(App(C(),F()),x666))))
6.34/2.49	   App(App(x543,App(App(App(C(),F()),x666),App(App(S(),App(S(),x543)),App(App(C(),F()),x666)))),
6.34/2.49	       App(App(App(S(),App(S(),x543)),App(App(C(),F()),x666)),App(App(App(C(),F()),x666),
6.34/2.49	                                                                  App
6.34/2.49	                                                                  (App(S(),App(S(),x543)),
6.34/2.49	                                                                   App
6.34/2.49	                                                                   (App(C(),F()),x666)))))
6.34/2.49	  context:
6.34/2.49	   App(App(x543,App(App(App(C(),F()),x666),App(App(S(),App(S(),x543)),App(App(C(),F()),x666)))),[])
6.34/2.49	  substitution:
6.34/2.49	   x543 -> x543
6.34/2.49	   x666 -> x666
6.34/2.49	  Qed
6.34/2.49	
6.44/2.53	EOF