Reducing the size of resolution proofs in linear time

  Abstract