6.55/2.60	MAYBE
6.55/2.60	
6.55/2.60	Proof:
6.55/2.60	ConCon could not decide confluence of the system.
6.55/2.60	\cite{ALS94}, Theorem 4.1 does not apply.
6.55/2.60	This system is of type 3 or smaller.
6.55/2.60	This system is strongly deterministic.
6.55/2.60	This system is of type 3 or smaller.
6.55/2.60	This system is deterministic.
6.55/2.60	This system is non-terminating.
6.55/2.60	Call external tool:
6.55/2.60	./ttt2.sh
6.55/2.60	Input:
6.55/2.60	(VAR x y z)
6.55/2.60	(RULES
6.55/2.60	  App(App(App(S, x), y), z) -> App(App(x, z), App(y, z))
6.55/2.60	  App(App(K, x), y) -> x
6.55/2.60	  App(I, x) -> x
6.55/2.60	  App(App(App(C, T), x), y) -> x
6.55/2.60	  App(App(App(C, F), x), y) -> y
6.55/2.60	  App(App(App(C, z), x), y) -> x
6.55/2.60	  App(App(App(C, z), x), y) -> y
6.55/2.60	  App(x, y) -> x
6.55/2.60	  App(x, y) -> y
6.55/2.60	)
6.55/2.60	
6.55/2.60	 Unfolding Processor:
6.55/2.60	  loop length: 3
6.55/2.60	  terms:
6.55/2.60	   App(App(App(S(),App(S(),x391)),I()),App(App(S(),App(S(),x391)),I()))
6.55/2.60	   App(App(App(S(),x391),App(App(S(),App(S(),x391)),I())),App(I(),App(App(S(),App(S(),x391)),I())))
6.55/2.60	   App(App(x391,App(I(),App(App(S(),App(S(),x391)),I()))),App(App(App(S(),App(S(),x391)),I()),
6.55/2.60	                                                              App(I(),
6.55/2.60	                                                                  App
6.55/2.60	                                                                  (App(S(),App(S(),x391)),I()))))
6.55/2.60	  context: App(App(x391,App(I(),App(App(S(),App(S(),x391)),I()))),[])
6.55/2.60	  substitution:
6.55/2.60	   x391 -> x391
6.55/2.61	  Qed
6.55/2.61	ConCon could not decide if this system is quasi-decreasing.
6.55/2.61	\cite{A14}, Theorem 11.5.9 does not apply.
6.55/2.61	This system is of type 3 or smaller.
6.55/2.61	This system is deterministic.
6.55/2.61	This system is non-terminating.
6.55/2.61	Call external tool:
6.55/2.61	./ttt2.sh
6.55/2.61	Input:
6.55/2.61	(VAR x y z)
6.55/2.61	(RULES
6.55/2.61	  App(App(App(S, x), y), z) -> App(App(x, z), App(y, z))
6.55/2.61	  App(App(K, x), y) -> x
6.55/2.61	  App(I, x) -> x
6.55/2.61	  App(App(App(C, T), x), y) -> x
6.55/2.61	  App(App(App(C, F), x), y) -> y
6.55/2.61	  App(App(App(C, z), x), y) -> x
6.55/2.61	  App(App(App(C, z), x), y) -> y
6.55/2.61	  App(x, y) -> x
6.55/2.61	  App(x, y) -> y
6.55/2.61	)
6.55/2.61	
6.55/2.61	 Unfolding Processor:
6.55/2.61	  loop length: 3
6.55/2.61	  terms:
6.55/2.61	   App(App(App(S(),App(S(),x391)),I()),App(App(S(),App(S(),x391)),I()))
6.55/2.61	   App(App(App(S(),x391),App(App(S(),App(S(),x391)),I())),App(I(),App(App(S(),App(S(),x391)),I())))
6.55/2.61	   App(App(x391,App(I(),App(App(S(),App(S(),x391)),I()))),App(App(App(S(),App(S(),x391)),I()),
6.55/2.61	                                                              App(I(),
6.55/2.61	                                                                  App
6.55/2.61	                                                                  (App(S(),App(S(),x391)),I()))))
6.55/2.61	  context: App(App(x391,App(I(),App(App(S(),App(S(),x391)),I()))),[])
6.55/2.61	  substitution:
6.55/2.61	   x391 -> x391
6.55/2.61	  Qed
6.55/2.61	
6.68/2.66	EOF