Input TRS:
    1: implies(not(x),y) -> or(x,y)
    2: implies(not(x),or(y,z)) -> implies(y,or(x,z))
    3: implies(x,or(y,z)) -> or(y,implies(x,z))
Number of strict rules: 3
Direct Order(PosReal,>,Poly) ... removes: 1 2
    or(x1,x2)	weight: 20653 + 2 * x1 + x2
implies(x1,x2)	weight: 8366 + x1 + x2
   not(x1)	weight: 12288 + 2 * x1
Number of strict rules: 1
Direct Order(PosReal,>,Poly) ... removes: 3
    or(x1,x2)	weight: (/ 1 4) + 2 * x1 + x2
implies(x1,x2)	weight: (/ 33461 4) + x1 + 2 * x2
   not(x1)	weight: (/ 49149 4) + 2 * x1
Number of strict rules: 0
YES