MAYBE Proof: ConCon could not decide if this system is quasi-decreasing. \cite{O02}, p. 214, Proposition 7.2.50 does not apply. System R transformed to U(R). Call external tool: ttt2 - trs 30 Input: ?2(c(y), x) -> k(y) ?1(d, x) -> ?2(h(x), x) g(x) -> ?1(h(x), x) h(d) -> c(a) h(d) -> c(b) f(k(a), k(b), x) -> f(x, x, x) The external tool could not decide termination.