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: ?1(y, x, y, z) -> G(z) F(x, y, z) -> ?1(x, x, y, z) G(A) -> F(A, B, A) e(x) -> f(x, x) f(x, y) -> x The external tool could not decide termination.