YES We show the termination of the TRS R: c(z,x,a()) -> f(b(b(f(z),z),x)) b(y,b(z,a())) -> f(b(c(f(a()),y,z),z)) f(c(c(z,a(),a()),x,a())) -> z -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: c#(z,x,a()) -> f#(b(b(f(z),z),x)) p2: c#(z,x,a()) -> b#(b(f(z),z),x) p3: c#(z,x,a()) -> b#(f(z),z) p4: c#(z,x,a()) -> f#(z) p5: b#(y,b(z,a())) -> f#(b(c(f(a()),y,z),z)) p6: b#(y,b(z,a())) -> b#(c(f(a()),y,z),z) p7: b#(y,b(z,a())) -> c#(f(a()),y,z) p8: b#(y,b(z,a())) -> f#(a()) and R consists of: r1: c(z,x,a()) -> f(b(b(f(z),z),x)) r2: b(y,b(z,a())) -> f(b(c(f(a()),y,z),z)) r3: f(c(c(z,a(),a()),x,a())) -> z The estimated dependency graph contains the following SCCs: {p2, p3, p6, p7} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: c#(z,x,a()) -> b#(b(f(z),z),x) p2: b#(y,b(z,a())) -> c#(f(a()),y,z) p3: c#(z,x,a()) -> b#(f(z),z) p4: b#(y,b(z,a())) -> b#(c(f(a()),y,z),z) and R consists of: r1: c(z,x,a()) -> f(b(b(f(z),z),x)) r2: b(y,b(z,a())) -> f(b(c(f(a()),y,z),z)) r3: f(c(c(z,a(),a()),x,a())) -> z The set of usable rules consists of r1, r2, r3 Take the reduction pair: weighted path order base order: max/plus interpretations on natural numbers: c#_A(x1,x2,x3) = max{x1 + 52, x2 + 2, x3 - 28} a_A = 65 b#_A(x1,x2) = max{x1 + 3, x2 + 1} b_A(x1,x2) = max{36, x1 + 13, x2 - 14} f_A(x1) = max{0, x1 - 65} c_A(x1,x2,x3) = max{x1 + 33, x2 - 13, x3 + 1} precedence: a > c# = b# = b = f = c partial status: pi(c#) = [1] pi(a) = [] pi(b#) = [1] pi(b) = [] pi(f) = [] pi(c) = [3] The next rules are strictly ordered: p1 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: b#(y,b(z,a())) -> c#(f(a()),y,z) p2: c#(z,x,a()) -> b#(f(z),z) p3: b#(y,b(z,a())) -> b#(c(f(a()),y,z),z) and R consists of: r1: c(z,x,a()) -> f(b(b(f(z),z),x)) r2: b(y,b(z,a())) -> f(b(c(f(a()),y,z),z)) r3: f(c(c(z,a(),a()),x,a())) -> z The estimated dependency graph contains the following SCCs: {p1, p2, p3} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: b#(y,b(z,a())) -> c#(f(a()),y,z) p2: c#(z,x,a()) -> b#(f(z),z) p3: b#(y,b(z,a())) -> b#(c(f(a()),y,z),z) and R consists of: r1: c(z,x,a()) -> f(b(b(f(z),z),x)) r2: b(y,b(z,a())) -> f(b(c(f(a()),y,z),z)) r3: f(c(c(z,a(),a()),x,a())) -> z The set of usable rules consists of r1, r2, r3 Take the reduction pair: weighted path order base order: max/plus interpretations on natural numbers: b#_A(x1,x2) = x2 + 32 b_A(x1,x2) = max{x1 + 20, x2 + 25} a_A = 8 c#_A(x1,x2,x3) = max{x1 + 44, x3 + 52} f_A(x1) = max{2, x1 - 23} c_A(x1,x2,x3) = max{x1 + 34, x2 + 23, x3 + 26} precedence: b# = b = a = c# = f = c partial status: pi(b#) = [2] pi(b) = [] pi(a) = [] pi(c#) = [] pi(f) = [] pi(c) = [3] The next rules are strictly ordered: p1 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: c#(z,x,a()) -> b#(f(z),z) p2: b#(y,b(z,a())) -> b#(c(f(a()),y,z),z) and R consists of: r1: c(z,x,a()) -> f(b(b(f(z),z),x)) r2: b(y,b(z,a())) -> f(b(c(f(a()),y,z),z)) r3: f(c(c(z,a(),a()),x,a())) -> z The estimated dependency graph contains the following SCCs: {p2} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: b#(y,b(z,a())) -> b#(c(f(a()),y,z),z) and R consists of: r1: c(z,x,a()) -> f(b(b(f(z),z),x)) r2: b(y,b(z,a())) -> f(b(c(f(a()),y,z),z)) r3: f(c(c(z,a(),a()),x,a())) -> z The set of usable rules consists of r1, r2, r3 Take the reduction pair: weighted path order base order: max/plus interpretations on natural numbers: b#_A(x1,x2) = x2 + 12 b_A(x1,x2) = max{x1 + 18, x2 + 30} a_A = 1 c_A(x1,x2,x3) = max{x1 + 32, x2 + 14, x3 + 10} f_A(x1) = max{12, x1 - 16} precedence: b# = b = a = c = f partial status: pi(b#) = [2] pi(b) = [] pi(a) = [] pi(c) = [3] pi(f) = [] The next rules are strictly ordered: p1 We remove them from the problem. Then no dependency pair remains.