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