On semantic resolution with lemmaizing and contraction