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