Input TRS: 1: top(north(old(n),e,s,w)) -> top(east(n,e,s,w)) 2: top(north(new(n),old(e),s,w)) -> top(east(n,old(e),s,w)) 3: top(north(new(n),e,old(s),w)) -> top(east(n,e,old(s),w)) 4: top(north(new(n),e,s,old(w))) -> top(east(n,e,s,old(w))) 5: top(east(n,old(e),s,w)) -> top(south(n,e,s,w)) 6: top(east(old(n),new(e),s,w)) -> top(south(old(n),e,s,w)) 7: top(east(n,new(e),old(s),w)) -> top(south(n,e,old(s),w)) 8: top(east(n,new(e),s,old(w))) -> top(south(n,e,s,old(w))) 9: top(south(n,e,old(s),w)) -> top(west(n,e,s,w)) 10: top(south(old(n),e,new(s),w)) -> top(west(old(n),e,s,w)) 11: top(south(n,old(e),new(s),w)) -> top(west(n,old(e),s,w)) 12: top(south(n,e,new(s),old(w))) -> top(west(n,e,s,old(w))) 13: top(west(n,e,s,old(w))) -> top(north(n,e,s,w)) 14: top(west(old(n),e,s,new(w))) -> top(north(old(n),e,s,w)) 15: top(west(n,old(e),s,new(w))) -> top(north(n,old(e),s,w)) 16: top(west(n,e,old(s),new(w))) -> top(north(n,e,old(s),w)) 17: top(north(bot(),old(e),s,w)) -> top(east(bot(),old(e),s,w)) 18: top(north(bot(),e,old(s),w)) -> top(east(bot(),e,old(s),w)) 19: top(north(bot(),e,s,old(w))) -> top(east(bot(),e,s,old(w))) 20: top(east(old(n),bot(),s,w)) -> top(south(old(n),bot(),s,w)) 21: top(east(n,bot(),old(s),w)) -> top(south(n,bot(),old(s),w)) 22: top(east(n,bot(),s,old(w))) -> top(south(n,bot(),s,old(w))) 23: top(south(old(n),e,bot(),w)) -> top(west(old(n),e,bot(),w)) 24: top(south(n,old(e),bot(),w)) -> top(west(n,old(e),bot(),w)) 25: top(south(n,e,bot(),old(w))) -> top(west(n,e,bot(),old(w))) 26: top(west(old(n),e,s,bot())) -> top(north(old(n),e,s,bot())) 27: top(west(n,old(e),s,bot())) -> top(north(n,old(e),s,bot())) 28: top(west(n,e,old(s),bot())) -> top(north(n,e,old(s),bot())) e1: top(north(old(n),e,s,w)) ->= top(north(n,e,s,w)) [relative] e2: top(north(new(n),e,s,w)) ->= top(north(n,e,s,w)) [relative] e3: top(east(n,old(e),s,w)) ->= top(east(n,e,s,w)) [relative] e4: top(east(n,new(e),s,w)) ->= top(east(n,e,s,w)) [relative] e5: top(south(n,e,old(s),w)) ->= top(south(n,e,s,w)) [relative] e6: top(south(n,e,new(s),w)) ->= top(south(n,e,s,w)) [relative] e7: top(west(n,e,s,old(w))) ->= top(west(n,e,s,w)) [relative] e8: top(west(n,e,s,new(w))) ->= top(west(n,e,s,w)) [relative] e9: bot() ->= new(bot()) [relative] Dependency Pairs: #1: # top(north(new(n),old(e),s,w)) -> # top(east(n,old(e),s,w)) #2: # top(south(n,e,new(s),w)) -> # top(south(n,e,s,w)) [relative] #3: # top(east(n,new(e),s,w)) -> # top(east(n,e,s,w)) [relative] #4: # top(east(old(n),new(e),s,w)) -> # top(south(old(n),e,s,w)) #5: # top(west(n,e,s,old(w))) -> # top(north(n,e,s,w)) #6: # top(south(n,e,old(s),w)) -> # top(west(n,e,s,w)) #7: # top(south(n,old(e),new(s),w)) -> # top(west(n,old(e),s,w)) #8: # top(south(n,old(e),bot(),w)) -> # top(west(n,old(e),bot(),w)) #9: # top(south(old(n),e,bot(),w)) -> # top(west(old(n),e,bot(),w)) #10: # top(south(n,e,new(s),old(w))) -> # top(west(n,e,s,old(w))) #11: # top(west(n,e,s,new(w))) -> # top(west(n,e,s,w)) [relative] #12: # top(west(old(n),e,s,new(w))) -> # top(north(old(n),e,s,w)) #13: # top(north(new(n),e,s,w)) -> # top(north(n,e,s,w)) [relative] #14: # top(south(n,e,bot(),old(w))) -> # top(west(n,e,bot(),old(w))) #15: # top(east(old(n),bot(),s,w)) -> # top(south(old(n),bot(),s,w)) #16: # top(east(n,new(e),old(s),w)) -> # top(south(n,e,old(s),w)) #17: # top(south(old(n),e,new(s),w)) -> # top(west(old(n),e,s,w)) #18: # top(east(n,old(e),s,w)) -> # top(east(n,e,s,w)) [relative] #19: # top(east(n,old(e),s,w)) -> # top(south(n,e,s,w)) #20: # top(west(n,e,old(s),bot())) -> # top(north(n,e,old(s),bot())) #21: # top(east(n,bot(),s,old(w))) -> # top(south(n,bot(),s,old(w))) #22: # top(south(n,e,old(s),w)) -> # top(south(n,e,s,w)) [relative] #23: # top(west(n,old(e),s,bot())) -> # top(north(n,old(e),s,bot())) #24: # top(north(bot(),old(e),s,w)) -> # top(east(bot(),old(e),s,w)) #25: # top(west(n,e,s,old(w))) -> # top(west(n,e,s,w)) [relative] #26: # top(north(bot(),e,s,old(w))) -> # top(east(bot(),e,s,old(w))) #27: # top(west(old(n),e,s,bot())) -> # top(north(old(n),e,s,bot())) #28: # top(north(old(n),e,s,w)) -> # top(north(n,e,s,w)) [relative] #29: # top(east(n,bot(),old(s),w)) -> # top(south(n,bot(),old(s),w)) #30: # top(west(n,e,old(s),new(w))) -> # top(north(n,e,old(s),w)) #31: # top(north(new(n),e,old(s),w)) -> # top(east(n,e,old(s),w)) #32: # top(north(old(n),e,s,w)) -> # top(east(n,e,s,w)) #33: # top(east(n,new(e),s,old(w))) -> # top(south(n,e,s,old(w))) #34: # top(west(n,old(e),s,new(w))) -> # top(north(n,old(e),s,w)) #35: # top(north(new(n),e,s,old(w))) -> # top(east(n,e,s,old(w))) #36: # top(north(bot(),e,old(s),w)) -> # top(east(bot(),e,old(s),w)) Number of SCCs: 1 SCC { #1..36 } POLO(Sum)... removes: #18 #19 #28 #32 I(new) = max(x1, 0) I(south) = max(x1 + x2, 0) I(top) = 0 I(bot) = 1 I(west) = max(x1 + x2, 0) I(north) = max(x1 + x2, 0) I(# top) = max(x1 + 1, 0) I(east) = max(x1 + x2, 0) I(old) = max(x1 + 1, 0) Number of SCCs: 1 SCC { #2..11 #13..17 #20..23 #25 #26 #29..31 #33..36 } POLO(Sum)... removes: #6 #22 I(new) = max(x1, 0) I(south) = max(x2 + x3 - 3, 0) I(top) = 0 I(bot) = 1 I(west) = max(x2 + x3 - 3, 0) I(north) = max(x2 + x3 - 3, 0) I(# top) = max(x1 + 1, 0) I(east) = max(x2 + x3 - 3, 0) I(old) = max(x1 + 4, 0) Number of SCCs: 1 SCC { #2..5 #7..11 #13..15 #17 #20 #21 #23 #25 #26 #30 #31 #33..36 } POLO(Sum)... removes: #5 #25 I(new) = max(x1, 0) I(south) = max(x1 + x4 + 1, 0) I(top) = 1 I(bot) = 1 I(west) = max(x1 + x4 + 1, 0) I(north) = max(x1 + x4 + 1, 0) I(# top) = max(x1 + 1, 0) I(east) = max(x1 + x4 + 1, 0) I(old) = max(x1 + 1, 0) Number of SCCs: 1 SCC { #2..4 #7..9 #11 #13 #15 #17 #20 #21 #23 #26 #30 #31 #33..36 } POLO(Sum)... QLPOS... QWPOpS(mSum)... Mat2b... removes: #4 #7 #8 #15 #20 #21 #23 #26 #30 #31 #33 #34 #35 #36 I(new) = [1,1;1,1] * x1 I(south) = [1,1;1,1] * x1 + [1,1;0,0] * x2 + [1,0;0,0] * x3 + [1,1;0,0] * x4 + [1;1] I(top) = [0;0] I(bot) = [0;0] I(west) = [1,0;0,0] * x1 + [0,1;1,1] * x2 + x3 + [1,1;0,0] * x4 + [4;1] I(north) = [1,0;0,0] * x1 + [0,1;1,1] * x2 + [1,0;0,0] * x3 + [1,1;0,0] * x4 + [3;1] I(# top) = [1,0;0,0] * x1 I(east) = [1,1;0,0] * x1 + [0,1;0,0] * x2 + [1,0;1,0] * x3 + [1,1;0,0] * x4 + [2;1] I(old) = [1,1;0,0] * x1 + [9;3] Number of SCCs: 4 SCC { #11 } POLO(Sum)... QLPOS... QWPOpS(mSum)... Mat2b... failed.