YES Did not drop rules. Inlined conditions for 0 rules. Left-inlined conditions for 0 rules. Due to Ifrit-method removed 2 infeasible rules: f(c(x),c(c(y))) -> a(a(x)) | c(f(x,y)) ->* c(a(b())) f(c(c(c(x))),y) -> a(y) | c(f(c(x) ,c(c(y)))) ->* c(a(a(b()))) Did not use redundant rules method. INFEASIBLE because problem obtained from input is proven infeasible using TCAP on |(c(f(c(c(x1)),y)) ,c(f(c(x1) ,c(c(c(c(y))))))) ->* |(c(a(b())) ,c(a(a(b())))) where | is used as a fresh function symbol, since it is illegal in the input format.