Input TRS:
    1: top(ok(new(x))) -> top(check(x))
    2: top(ok(old(x))) -> top(check(x))
    3: bot() ->= new(bot())
    4: check(new(x)) ->= new(check(x))
    5: check(old(x)) ->= old(check(x))
    6: check(old(x)) ->= ok(old(x))
    7: new(ok(x)) ->= ok(new(x))
    8: old(ok(x)) ->= ok(old(x))
Number of strict rules: 2
Direct Order(PosReal,>,Poly) ... removes: 2
   new(x1)	weight: x1
   top(x1)	weight: x1
   bot()	weight: (/ 1 4)
 check(x1)	weight: (/ 170941 4) + x1
    ok(x1)	weight: (/ 170941 4) + x1
   old(x1)	weight: (/ 1 4) + x1
Number of strict rules: 1
Direct Order(PosReal,>,Poly) ... removes: 1 5 7 6
   new(x1)	weight: 2 * x1
   top(x1)	weight: x1
   bot()	weight: 0
 check(x1)	weight: 2 * x1
    ok(x1)	weight: (/ 52571 2) + x1
   old(x1)	weight: 26286 + x1
Number of strict rules: 0
YES