ABSTRACT. In this lecture we show, that a resolution refutation based on Andrew's Skolemization cannot be transformed into a cut-free LK-derivation within elementary bounds. It is however reducible almost immedeately to a cut-free LK++ derivation. (LK++ is LK with weakened but globally sound Eigenvariable conditions,) LK** derivations can be transformed without LK-derivations without increase of complexity. Therefore the use of Andrew's Skolemization corresponds to the introduction of complex cuts to resolution theorem proving. 

Juan Aguilera, Matthias Baaz: Unsound rules make proofs easier, 
Journal of symbolic logic (to appear)

ABSTRACT. Cooperation and competition play an import role in theorem provers and their development. The talk will illustrate this by by discussing some instances of either.