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