PreProcessor

Novelty: Removing Tautologies

• true literals (trivial tautologies)
• Regular tautologies
• Maintain the derivation structure

Simplification

• false literals
• Keep simplified clauses