YES Input TRS: 1: a() -> a() | f(a()) --> a() 2: f(x) -> a() | x --> b() Infeasibility test: f(a()) --> a() Co-Order(NegReal,≥,Sum) ... succeeded. a() weight: (- (/ 1 2)) b() weight: 0 f(x1) weight: (- (/ 1 2)) + x1 #(x1) weight: x1