YES Proof: This system is confluent. By \cite{ALS94}, Theorem 4.1. This system is of type 3 or smaller. This system is strongly deterministic. All 8 critical pairs are joinable. s(e) = t(l): This critical pair is not unfeasible. This critical pair is context-joinable. d = c: This critical pair is not unfeasible. This critical pair is context-joinable. t(k) = t(l): This critical pair is not unfeasible. This critical pair is context-joinable. s(e) = t(k): This critical pair is not unfeasible. This critical pair is context-joinable. d = c: This critical pair is not unfeasible. This critical pair is context-joinable. c = d: This critical pair is not unfeasible. This critical pair is context-joinable. c = d: This critical pair is not unfeasible. This critical pair is context-joinable. t(l) = t(k): This critical pair is not unfeasible. This critical pair is context-joinable. By \cite{A14}, Theorem 11.5.9. This system is of type 3 or smaller. This system is deterministic. System R transformed to V(R) + Emb. Call external tool: ttt2 - trs 30 Input: a -> c a -> d b -> c b -> d c -> e d -> e k -> e l -> e s(c) -> t(k) s(c) -> t(l) s(e) -> t(e) g(x, x) -> h(x, x) f(x) -> pair(x, s(x)) f(x) -> s(x) h(x, y) -> x h(x, y) -> y pair(x, y) -> x pair(x, y) -> y s(x) -> x g(x, y) -> x g(x, y) -> y t(x) -> x f(x) -> x DP Processor: DPs: a#() -> c#() a#() -> d#() b#() -> c#() b#() -> d#() s#(c()) -> k#() s#(c()) -> t#(k()) s#(c()) -> l#() s#(c()) -> t#(l()) s#(e()) -> t#(e()) g#(x,x) -> h#(x,x) f#(x) -> s#(x) f#(x) -> pair#(x,s(x)) TRS: a() -> c() a() -> d() b() -> c() b() -> d() c() -> e() d() -> e() k() -> e() l() -> e() s(c()) -> t(k()) s(c()) -> t(l()) s(e()) -> t(e()) g(x,x) -> h(x,x) f(x) -> pair(x,s(x)) f(x) -> s(x) h(x,y) -> x h(x,y) -> y pair(x,y) -> x pair(x,y) -> y s(x) -> x g(x,y) -> x g(x,y) -> y t(x) -> x f(x) -> x TDG Processor: DPs: a#() -> c#() a#() -> d#() b#() -> c#() b#() -> d#() s#(c()) -> k#() s#(c()) -> t#(k()) s#(c()) -> l#() s#(c()) -> t#(l()) s#(e()) -> t#(e()) g#(x,x) -> h#(x,x) f#(x) -> s#(x) f#(x) -> pair#(x,s(x)) TRS: a() -> c() a() -> d() b() -> c() b() -> d() c() -> e() d() -> e() k() -> e() l() -> e() s(c()) -> t(k()) s(c()) -> t(l()) s(e()) -> t(e()) g(x,x) -> h(x,x) f(x) -> pair(x,s(x)) f(x) -> s(x) h(x,y) -> x h(x,y) -> y pair(x,y) -> x pair(x,y) -> y s(x) -> x g(x,y) -> x g(x,y) -> y t(x) -> x f(x) -> x graph: f#(x) -> s#(x) -> s#(e()) -> t#(e()) f#(x) -> s#(x) -> s#(c()) -> t#(l()) f#(x) -> s#(x) -> s#(c()) -> l#() f#(x) -> s#(x) -> s#(c()) -> t#(k()) f#(x) -> s#(x) -> s#(c()) -> k#() SCC Processor: #sccs: 0 #rules: 0 #arcs: 5/144 This system is deterministic. This system is not weakly left-linear. This system is not normal. This system is oriented. This system is of type 3 or smaller. This system is right-stable. This system is properly oriented. This is not an overlay system. This system is conditional.