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(B, x) -> F(A) F(x) -> ?1(x, x) e(x) -> x LPO Processor: precedence: B > F > e ~ A ~ ?1 problem: Qed