YES Input TRS: 1: pin(a()) -> pout(b()) 2: pin(b()) -> pout(c()) 3: tc(x) -> x 4: tc(x) -> y | pin(x) --> pout(z()) | tc(z()) --> y Infeasibility test: pin(x1) --> pout(z()) tc(z()) --> x2 Symbol transition graph: tc --> # a b c pin pout tc z pin --> pout Collapsable symbols: { tc tc }