We have experimented a UP-based pre-treatment to eliminate redundant clauses in SAT instances extensively on the last SAT competitions benchmarks ( http://www.satcompetition.org). We have tested more than 700 SAT instances which are from various domains (industrial, random,handmade, graph-coloring, ...). Three of the winners of the last three competitions, namely ZChaff, Minisat and SatElite have been selected as SAT solvers. All experiments have been conducted on Pentium IV, 3Ghz under linux Fedora Core 4.