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 Rules: 8
Direct QTKBOS ... orients all.
	I(.) = 3 * x1 + x2 + 1	sigma(.) = [2,1]
	I(car) = 3 * x1 + 3	sigma(car) = [1]
	I(nil) = 2
	I(++) = x1 + 2 * x2	sigma(++) = [2,1]
	I(cdr) = 3 * x1	sigma(cdr) = [1]
	I(null) = 3 * x1	sigma(null) = [1]
	I(rev) = 3 * x1 + 1	sigma(rev) = [1]
	I(true) = 2
	I(false) = 1
    PREC: cdr = null > rev > true > ++ > . > car = nil = false
Number of Rules: 0