Reduction rules and universal variables for first order tableaux and DPLL