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.