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