YES(?,O(n^2)) TRS: { a__c X -> d X, a__c X -> c X, a__f X -> f X, a__f f X -> a__c f g f X, a__h X -> h X, a__h X -> a__c d X, mark f X -> a__f mark X, mark g X -> g X, mark h X -> a__h mark X, mark d X -> d X, mark c X -> a__c X } DUP: We consider a non-duplicating system. Trs: { a__c X -> d X, a__c X -> c X, a__f X -> f X, a__f f X -> a__c f g f X, a__h X -> h X, a__h X -> a__c d X, mark f X -> a__f mark X, mark g X -> g X, mark h X -> a__h mark X, mark d X -> d X, mark c X -> a__c X } Matrix Interpretation: Interpretation class: triangular [X1] [1 0][X1] [0] [c]([X0]) = [0 0][X0] + [1] [X1] [1 2][X1] [1] [mark]([X0]) = [0 1][X0] + [0] [X1] [1 2][X1] [3] [a__h]([X0]) = [0 1][X0] + [1] [X1] [1 0][X1] [0] [d]([X0]) = [0 0][X0] + [0] [X1] [1 2][X1] [1] [a__f]([X0]) = [0 1][X0] + [1] [X1] [1 0][X1] [2] [a__c]([X0]) = [0 0][X0] + [1] [X1] [1 2][X1] [2] [h]([X0]) = [0 1][X0] + [1] [X1] [1 0][X1] [0] [g]([X0]) = [0 0][X0] + [0] [X1] [1 2][X1] [0] [f]([X0]) = [0 1][X0] + [1] Qed