MAYBE

Proof:
ConCon could not decide if this system is quasi-decreasing.
\cite{A14}, Theorem 11.5.9 does not apply.
System R transformed to V(R) + Emb.
Call external tool:
ttt2 - trs 30
Input:
  g(x) -> k(h(x))
  g(x) -> h(x)
  h(d) -> c(a)
  h(d) -> c(b)
  f(k(a), k(b), x) -> f(x, x, x)
  h(x) -> x
  c(x) -> x
  k(x) -> x
  g(x) -> x
  f(x, y, z) -> x
  f(x, y, z) -> y
  f(x, y, z) -> z

The external tool could not decide termination.