YES Input TRS: 1: g(a(),y) -> y 2: f(x,a()) -> f(x,g(x,b())) 3: g(h(x),y) -> g(x,h(y)) Infeasibility test: F(x,g(x,b())) --> F(y,a()) Co-Order(NegReal,≥,Sum) ... succeeded. a() weight: (- (/ 1 2)) h(x1) weight: (- (/ 1 2)) + x1 b() weight: -2438 F(x1,x2) weight: x2 f(x1,x2) weight: x2 #(x1) weight: x1 g(x1,x2) weight: x2