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