Input TRS: 1: f(b(x),y) -> f(x,b(y)) 2: f(x,a(y)) -> f(a(x),y) e1: f(x,y) ->= f(a(x),y) [relative] e2: f(x,y) ->= f(x,b(y)) [relative] Dependency Pairs: #1: # f(x,a(y)) -> # f(a(x),y) #2: # f(x,y) -> # f(x,b(y)) [relative] #3: # f(b(x),y) -> # f(x,b(y)) #4: # f(x,y) -> # f(a(x),y) [relative] Number of SCCs: 1 SCC { #1..4 } POLO(Sum)... removes: #3 I(a) = max(x1 - 1, 0) I(b) = max(x1 + 2, 0) I(# f) = max(x1 - 1, 0) USABLE RULES: { } Number of SCCs: 1 SCC { #1 #2 #4 } POLO(Sum)... removes: #1 I(a) = max(x1 + 1, 0) I(b) = 0 I(# f) = max(x2 + 1, 0) USABLE RULES: { } Number of SCCs: 1 SCC { #2 #4 } POLO(Sum)... QLPOS... QWPOpS(mSum)... Mat2b... failed.