MAYBE Proof: ConCon could not decide confluence of the system. \cite{ALS94}, Theorem 4.1 does not apply. \cite{A14}, Theorem 11.5.9 does not apply. \cite{O02}, p. 214, Proposition 7.2.50 does not apply. System R transformed to optimized U(R). Call external tool: ttt2 - trs 30 Input: ?1(I, a, b, c) -> App(App(a, c), App(b, c)) ?2(I, a, b, c) -> ?1(c, a, b, c) ?3(I, a, b, c) -> ?2(b, a, b, c) App(App(App(S, a), b), c) -> ?3(a, a, b, c) ?4(I, a, b) -> a ?5(I, a, b) -> ?4(b, a, b) App(App(K, a), b) -> ?5(a, a, b) ?6(I, a) -> a App(I, a) -> ?6(a, a) The external tool could not decide termination. \cite{O02}, p. 214, Proposition 7.2.50 does not apply. System R transformed to U(R). Call external tool: ttt2 - trs 30 Input: ?3(I, a, b, c) -> App(App(a, c), App(b, c)) ?2(I, a, b, c) -> ?3(c, a, b, c) ?1(I, a, b, c) -> ?2(b, a, b, c) App(App(App(S, a), b), c) -> ?1(a, a, b, c) ?5(I, a, b) -> a ?4(I, a, b) -> ?5(b, a, b) App(App(K, a), b) -> ?4(a, a, b) ?6(I, a) -> a App(I, a) -> ?6(a, a) The external tool could not decide termination.