Input TRS: 1: f(a()) -> f(c(a())) 2: f(c(X)) -> X 3: f(c(a())) -> f(d(b())) 4: f(a()) -> f(d(a())) 5: f(d(X)) -> X 6: f(c(b())) -> f(d(a())) 7: e(g(X)) -> e(X) Number of strict rules: 7 Direct Order(PosReal,>,Poly) ... removes: 5 7 2 a() weight: 0 d(x1) weight: x1 b() weight: 0 c(x1) weight: x1 f(x1) weight: (/ 1 4) + x1 e(x1) weight: 2 * x1 g(x1) weight: (/ 1 4) + x1 Number of strict rules: 4 Direct Order(PosReal,>,Poly) ... failed. Freezing f 1: f❆1_a() -> f❆1_c(a()) 3: f❆1_c(a()) -> f❆1_d(b()) 4: f❆1_a() -> f❆1_d(a()) 6: f❆1_c(b()) -> f❆1_d(a()) 8: f(a()) ->= f❆1_a() 9: f(d(_1)) ->= f❆1_d(_1) 10: f(c(_1)) ->= f❆1_c(_1) Number of strict rules: 4 Direct Order(PosReal,>,Poly) ... removes: 8 10 9 a() weight: 0 d(x1) weight: (/ 30877 4) + x1 b() weight: 0 c(x1) weight: (/ 1 4) + x1 f❆1_c(x1) weight: x1 f(x1) weight: (/ 1 4) + 2 * x1 e(x1) weight: x1 f❆1_d(x1) weight: x1 f❆1_a() weight: 0 g(x1) weight: x1 Number of strict rules: 4 Direct Order(PosReal,>,Poly) ... failed. Dependency Pairs: #1: #f❆1_a() -> #f❆1_c(a()) Number of SCCs: 0, DPs: 0, edges: 0 YES