YES Input TRS: 1: f(x,x) -> c() 2: a() -> b() 3: b() -> a() Infeasibility test: f(a(),c()) --> b() Symbol transition graph: a --> a b b --> a b f --> c Collapsable symbols: { }