YES
exiting with thread!
(VAR u v x y z )
(RULES 
        eq(x,x) -> true
        eq(nil,end(y,z)) -> false
        eq(end(x,y),nil) -> false
        eq(end(x,y),end(u,v)) -> and(eq(y,v),eq(x,u))
        f(x,nil) -> end(nil,x)
        f(x,end(y,z)) -> end(f(x,y),z)
        .(nil,y) -> y
        .(end(x,y),z) -> .(x,f(y,z))
        null(nil) -> true
        null(end(x,y)) -> false
        and(true,true) -> true
        
)