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