Input TRS:
    1: rev(nil()) -> nil()
    2: rev(.(x,y)) -> ++(rev(y),.(x,nil()))
    3: car(.(x,y)) -> x
    4: cdr(.(x,y)) -> y
    5: null(nil()) -> true()
    6: null(.(x,y)) -> false()
    7: ++(nil(),y) -> y
    8: ++(.(x,y),z) -> .(x,++(y,z))
Number of strict rules: 8
Direct Order(PosReal,>,Poly) ... removes: 4 1 3 5 7 6 2
   cdr(x1)	weight: 2 * x1
    ++(x1,x2)	weight: (/ 164249 4) + x1 + x2
 false()	weight: 0
  true()	weight: 0
  null(x1)	weight: (/ 1 4) + 2 * x1
   nil()	weight: 0
   rev(x1)	weight: (/ 1 4) + 2 * x1
     .(x1,x2)	weight: (/ 82125 2) + 2 * x1 + x2
   car(x1)	weight: 2 * x1
Number of strict rules: 1
Direct Order(PosReal,>,Poly) ... removes: 8
   cdr(x1)	weight: 2 * x1
    ++(x1,x2)	weight: (/ 1 4) + 2 * x1 + x2
 false()	weight: 0
  true()	weight: 0
  null(x1)	weight: (/ 1 4) + 2 * x1
   nil()	weight: 0
   rev(x1)	weight: 2 * x1
     .(x1,x2)	weight: (/ 1 4) + 2 * x1 + x2
   car(x1)	weight: 2 * x1
Number of strict rules: 0
YES