Effective Skolemization.

We define a new relatively simple Skolemization method called atomic Skolemization which allows for a non-elementarily bounded speed-up of cut-free LK -proofs and resolution proofs w.r.t. the standard Skolemization and Andrews Skolemization.