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