0 QTRS
a__f(a, b, X) → a__f(X, X, mark(X)) a__c → a a__c → b mark(f(X1, X2, X3)) → a__f(X1, X2, mark(X3)) mark(c) → a__c mark(a) → a mark(b) → b a__f(X1, X2, X3) → f(X1, X2, X3) a__c → c