Input TRS:
    1: or(x,x) -> x
    2: and(x,x) -> x
    3: not(not(x)) -> x
    4: not(and(x,y)) -> or(not(x),not(y))
    5: not(or(x,y)) -> and(not(x),not(y))
Number of strict rules: 5
Direct Order(PosReal,>,Poly) ... removes: 1 2
   and(x1,x2)	weight: 20538 + x1 + x2
    or(x1,x2)	weight: 20538 + x1 + x2
   not(x1)	weight: x1
Number of strict rules: 3
Direct Order(PosReal,>,Poly) ... removes: 4 3 5
   and(x1,x2)	weight: 41074 + x1 + x2
    or(x1,x2)	weight: (/ 82149 4) + x1 + x2
   not(x1)	weight: (/ 1 4) + 2 * x1
Number of strict rules: 0
YES