Feasible computational methods in the propositional calculus