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(e, x) -> x f(x) -> ?1(x, x) ?2(x, x, y) -> A g(d, x, y) -> ?2(y, x, y) ?3(x, x, y) -> g(x, y, f(k)) h(x, y) -> ?3(y, x, y) a -> c a -> d b -> c b -> d c -> e c -> l k -> l k -> m d -> m DP Processor: DPs: f#(x) -> ?1#(x,x) g#(d(),x,y) -> ?2#(y,x,y) ?3#(x,x,y) -> k#() ?3#(x,x,y) -> f#(k()) ?3#(x,x,y) -> g#(x,y,f(k())) h#(x,y) -> ?3#(y,x,y) a#() -> c#() a#() -> d#() b#() -> c#() b#() -> d#() TRS: ?1(e(),x) -> x f(x) -> ?1(x,x) ?2(x,x,y) -> A() g(d(),x,y) -> ?2(y,x,y) ?3(x,x,y) -> g(x,y,f(k())) h(x,y) -> ?3(y,x,y) a() -> c() a() -> d() b() -> c() b() -> d() c() -> e() c() -> l() k() -> l() k() -> m() d() -> m() TDG Processor: DPs: f#(x) -> ?1#(x,x) g#(d(),x,y) -> ?2#(y,x,y) ?3#(x,x,y) -> k#() ?3#(x,x,y) -> f#(k()) ?3#(x,x,y) -> g#(x,y,f(k())) h#(x,y) -> ?3#(y,x,y) a#() -> c#() a#() -> d#() b#() -> c#() b#() -> d#() TRS: ?1(e(),x) -> x f(x) -> ?1(x,x) ?2(x,x,y) -> A() g(d(),x,y) -> ?2(y,x,y) ?3(x,x,y) -> g(x,y,f(k())) h(x,y) -> ?3(y,x,y) a() -> c() a() -> d() b() -> c() b() -> d() c() -> e() c() -> l() k() -> l() k() -> m() d() -> m() graph: h#(x,y) -> ?3#(y,x,y) -> ?3#(x,x,y) -> g#(x,y,f(k())) h#(x,y) -> ?3#(y,x,y) -> ?3#(x,x,y) -> f#(k()) h#(x,y) -> ?3#(y,x,y) -> ?3#(x,x,y) -> k#() ?3#(x,x,y) -> g#(x,y,f(k())) -> g#(d(),x,y) -> ?2#(y,x,y) ?3#(x,x,y) -> f#(k()) -> f#(x) -> ?1#(x,x) SCC Processor: #sccs: 0 #rules: 0 #arcs: 5/100