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: ?1(c) -> a a -> ?1(b) G(x, y) -> x G(x, y) -> y LPO Processor: precedence: c > a > G ~ b ~ ?1 problem: Qed