YES Proof: This system is quasi-decreasing. By \cite{O02}, p. 214, Proposition 7.2.50. This system is of type 3 or smaller. This system is deterministic. System R transformed to U(R). Call external tool: ttt2 - trs 30 Input: a -> c g(a) -> h(b) h(b) -> g(c) ?1(h(z), x) -> z f(x) -> ?1(g(x), x) LPO Processor: precedence: f > a > b > ?1 ~ h ~ g ~ c problem: Qed