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()))
    29: top(north(old(n),e,s,w)) ->= top(north(n,e,s,w))
    30: top(north(new(n),e,s,w)) ->= top(north(n,e,s,w))
    31: top(east(n,old(e),s,w)) ->= top(east(n,e,s,w))
    32: top(east(n,new(e),s,w)) ->= top(east(n,e,s,w))
    33: top(south(n,e,old(s),w)) ->= top(south(n,e,s,w))
    34: top(south(n,e,new(s),w)) ->= top(south(n,e,s,w))
    35: top(west(n,e,s,old(w))) ->= top(west(n,e,s,w))
    36: top(west(n,e,s,new(w))) ->= top(west(n,e,s,w))
    37: bot() ->= new(bot())
Number of strict rules: 28
Direct Order(PosReal,>,Poly) ... removes: 1 5 33 31 9 13 35 29
   new(x1)	weight: x1
 south(x1,x2,x3,x4)	weight: (/ 1 16) + x4 + x3 + x2 + x1
   top(x1)	weight: x1
   bot()	weight: (/ 1 16)
  west(x1,x2,x3,x4)	weight: (/ 1 16) + x4 + x3 + x2 + x1
 north(x1,x2,x3,x4)	weight: (/ 1 16) + x4 + x3 + x2 + x1
  east(x1,x2,x3,x4)	weight: (/ 1 16) + x4 + x3 + x2 + x1
   old(x1)	weight: (/ 1 16) + x1
Number of strict rules: 24
Direct Order(PosReal,>,Poly) ... removes: 16 28 24 11
   new(x1)	weight: 2 * x1
 south(x1,x2,x3,x4)	weight: (/ 1 8) + x4 + x3 + 2 * x2 + x1
   top(x1)	weight: x1
   bot()	weight: 0
  west(x1,x2,x3,x4)	weight: (/ 1 8) + x4 + 2 * x3 + x2 + x1
 north(x1,x2,x3,x4)	weight: (/ 1 8) + x4 + x3 + x2 + x1
  east(x1,x2,x3,x4)	weight: (/ 1 8) + x4 + x3 + x2 + x1
   old(x1)	weight: (/ 1 8) + x1
Number of strict rules: 20
Direct Order(PosReal,>,Poly) ... removes: 20 6
   new(x1)	weight: 2 * x1
 south(x1,x2,x3,x4)	weight: (/ 1 8) + x4 + x3 + x2 + x1
   top(x1)	weight: x1
   bot()	weight: 0
  west(x1,x2,x3,x4)	weight: (/ 1 8) + x4 + x3 + x2 + x1
 north(x1,x2,x3,x4)	weight: (/ 1 8) + x4 + x3 + x2 + x1
  east(x1,x2,x3,x4)	weight: (/ 1 8) + x4 + x3 + x2 + 2 * x1
   old(x1)	weight: (/ 1 8) + x1
Number of strict rules: 18
Direct Order(PosReal,>,Poly) ... removes: 15 27
   new(x1)	weight: 2 * x1
 south(x1,x2,x3,x4)	weight: x4 + 2 * x3 + 2 * x2 + x1
   top(x1)	weight: x1
   bot()	weight: 0
  west(x1,x2,x3,x4)	weight: x4 + 2 * x3 + 2 * x2 + x1
 north(x1,x2,x3,x4)	weight: x4 + 2 * x3 + x2 + x1
  east(x1,x2,x3,x4)	weight: x4 + 2 * x3 + x2 + x1
   old(x1)	weight: (/ 1 8) + 2 * x1
Number of strict rules: 16
Direct Order(PosReal,>,Poly) ... removes: 21 7
   new(x1)	weight: 2 * x1
 south(x1,x2,x3,x4)	weight: x4 + x3 + 2 * x2 + x1
   top(x1)	weight: x1
   bot()	weight: 0
  west(x1,x2,x3,x4)	weight: x4 + 2 * x3 + 2 * x2 + x1
 north(x1,x2,x3,x4)	weight: x4 + 2 * x3 + x2 + x1
  east(x1,x2,x3,x4)	weight: x4 + 2 * x3 + x2 + x1
   old(x1)	weight: (/ 1 8) + 2 * x1
Number of strict rules: 14
Direct Order(PosReal,>,Poly) ... removes: 18 4 8 3 19 17 22 10 25 12 23 2
   new(x1)	weight: 2 * x1
 south(x1,x2,x3,x4)	weight: (/ 79687 4) + x4 + x3 + x2 + 2 * x1
   top(x1)	weight: 2 * x1
   bot()	weight: 0
  west(x1,x2,x3,x4)	weight: (/ 35253 2) + x4 + x3 + x2 + 2 * x1
 north(x1,x2,x3,x4)	weight: (/ 79689 4) + 2 * x4 + x3 + x2 + x1
  east(x1,x2,x3,x4)	weight: 19922 + x4 + x3 + x2 + 2 * x1
   old(x1)	weight: (/ 9183 4) + 2 * x1
Number of strict rules: 2
Direct Order(PosReal,>,Poly) ... removes: 26 14
   new(x1)	weight: 2 * x1
 south(x1,x2,x3,x4)	weight: (/ 1 8) + x4 + x3 + x2 + 2 * x1
   top(x1)	weight: 2 * x1
   bot()	weight: 0
  west(x1,x2,x3,x4)	weight: (/ 1 8) + x4 + x3 + x2 + 2 * x1
 north(x1,x2,x3,x4)	weight: (/ 3 16) + 2 * x4 + x3 + x2 + x1
  east(x1,x2,x3,x4)	weight: (/ 1 8) + x4 + x3 + x2 + 2 * x1
   old(x1)	weight: (/ 1 8) + 2 * x1
Number of strict rules: 0
YES