Input TRS:
    1: a__and(tt(),X) -> mark(X)
    2: a__plus(N,0()) -> mark(N)
    3: a__plus(N,s(M)) -> s(a__plus(mark(N),mark(M)))
    4: mark(and(X1,X2)) -> a__and(mark(X1),X2)
    5: mark(plus(X1,X2)) -> a__plus(mark(X1),mark(X2))
    6: mark(tt()) -> tt()
    7: mark(0()) -> 0()
    8: mark(s(X)) -> s(mark(X))
    9: a__and(X1,X2) -> and(X1,X2)
    10: a__plus(X1,X2) -> plus(X1,X2)
Number of strict rules: 10
Direct Order(PosReal,>,Poly) ... removes: 1 2
a__plus(x1,x2)	weight: (/ 112401 4) + x1 + x2
     s(x1)	weight: (/ 1 4) + x1
   and(x1,x2)	weight: (/ 4569 4) + x1 + x2
     0()	weight: 0
  mark(x1)	weight: x1
  plus(x1,x2)	weight: (/ 112401 4) + x1 + x2
    tt()	weight: 0
a__and(x1,x2)	weight: (/ 4569 4) + x1 + x2
Number of strict rules: 8
Direct Order(PosReal,>,Poly) ... removes: 3
a__plus(x1,x2)	weight: (/ 112401 4) + x1 + 2 * x2
     s(x1)	weight: (/ 1 4) + x1
   and(x1,x2)	weight: (/ 4569 4) + x1 + x2
     0()	weight: 0
  mark(x1)	weight: x1
  plus(x1,x2)	weight: (/ 112401 4) + x1 + 2 * x2
    tt()	weight: 0
a__and(x1,x2)	weight: (/ 4569 4) + x1 + x2
Number of strict rules: 7
Direct Order(PosReal,>,Poly) ... removes: 8 10 9
a__plus(x1,x2)	weight: (/ 95123 2) + x1 + x2
     s(x1)	weight: (/ 1 4) + x1
   and(x1,x2)	weight: (/ 4569 8) + x1 + x2
     0()	weight: 0
  mark(x1)	weight: 2 * x1
  plus(x1,x2)	weight: (/ 95123 4) + x1 + x2
    tt()	weight: 0
a__and(x1,x2)	weight: (/ 4569 4) + x1 + 2 * x2
Number of strict rules: 4
Direct Order(PosReal,>,Poly) ... removes: 4 5
a__plus(x1,x2)	weight: (/ 95123 2) + x1 + x2
     s(x1)	weight: (/ 1 4) + x1
   and(x1,x2)	weight: (/ 1 4) + 2 * x1 + x2
     0()	weight: 0
  mark(x1)	weight: 2 * x1
  plus(x1,x2)	weight: (/ 190247 8) + x1 + x2
    tt()	weight: 0
a__and(x1,x2)	weight: (/ 1 4) + x1 + 2 * x2
Number of strict rules: 2
Direct Order(PosReal,>,Poly) ... removes: 7 6
a__plus(x1,x2)	weight: (/ 190245 4) + x1 + x2
     s(x1)	weight: (/ 1 4) + 2 * x1
   and(x1,x2)	weight: (/ 1 8) + 2 * x1 + x2
     0()	weight: 0
  mark(x1)	weight: (/ 1 8) + 2 * x1
  plus(x1,x2)	weight: (/ 380491 16) + x1 + x2
    tt()	weight: 0
a__and(x1,x2)	weight: (/ 1 4) + x1 + 2 * x2
Number of strict rules: 0
YES