Input TRS: 1: top(old(x)) -> top(check(x)) 2: top(new(x)) -> top(check(x)) e1: bot() ->= new(bot()) [relative] e2: check(new(x)) ->= new(check(x)) [relative] e3: check(old(x)) ->= old(check(x)) [relative] e4: check(old(x)) ->= old(x) [relative] Number of Rules: 2 Direct POLO(Sum) ... removes: 1 I(new) = x1 I(top) = x1 I(bot) = 0 I(check) = x1 I(old) = x1 + 1 Number of Rules: 1 Direct POLO(Sum) ...Direct Mat2b ... removes: e3 e4 I(new) = [2,0;1,0] * x1 + [0;1] I(top) = [2,1;0,1] * x1 I(bot) = [0;1] I(check) = [2,0;1,0] * x1 + [0;1] I(old) = [1,0;0,0] * x1 + [1;1] Number of Rules: 1 Direct POLO(Sum) ...Direct Mat2b ...Direct Mat3b ... failed. Dependency Pairs: #1: # top(new(x)) -> # top(check(x)) Number of SCCs: 1 SCC { #1 } POLO(Sum)... QLPOS... QWPOpS(mSum)... Mat3b... failed.