# Parsed axioms : 1
# SZS output end CNFRefutation.
# SZS output start CNFRefutation.
# SZS status Theorem